The general idea is that formal methods are self-verifying, up to a point. Sloppy formal methods simply won't prove.
The point up to which formal methods stops is: do the formally encoded requirements actually encode what I want to be true?
One can make the argument that the requirements is a much smaller surface to verify than that of the entire program.
The counter argument is that figuring out what you want the program to do has always been the hardest part of programming, and that programming in itself is a journey to discover latent requirements.
> One can make the argument that the requirements is a much smaller surface to verify than that of the entire program.
This argument is unfortunately empirically false for any program of any meaningful complexity (>1000 lines, probably even as low as >100 lines ignoring well-defined algorithms and data structures) using current formal methods.
Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase.
So, it is both harder to figure out if you encoded the desired requirements and it is more complex. Your only advantage is confidence that what you wrote down is proven.
> Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase.
Is it possible that the spec could be factorised into something higher-level and more modular? If not, can you give a flavour of the type of unavoidable esoteric detail? (One area I can see lots of complications is when dealing with versioned data, especially in multiple interacting systems -- naively, correctness needs to be proven for every combination of versions, even if some are never seen.)
The point up to which formal methods stops is: do the formally encoded requirements actually encode what I want to be true?
One can make the argument that the requirements is a much smaller surface to verify than that of the entire program.
The counter argument is that figuring out what you want the program to do has always been the hardest part of programming, and that programming in itself is a journey to discover latent requirements.