I did a course on formal methods at university. The 'spec' ended up being a lot more complicated than the actual program.
I wasn't really confident afterwards that the "proved" software actually did work.
I think it's possibly a suitable method for building very low level code (e.g. sorting methods) where the spec is going to be exceptionally simple but it's effectiveness drops off quickly the higher up the stack you go.
I did a course on formal methods at university. The 'spec' ended up being a lot more complicated than the actual program.
I wasn't really confident afterwards that the "proved" software actually did work.
I think it's possibly a suitable method for building very low level code (e.g. sorting methods) where the spec is going to be exceptionally simple but it's effectiveness drops off quickly the higher up the stack you go.