3 ms·
I agree that formal verification can create more work to write programs, but you get a lot more time back in debugging and readability
by sesuximo 7y ago
I agree that formal verification can create more work to write programs, but you get a lot more time back in debugging and readability
- tsimionescu 7y agoThat is simply not true empirically. Formal verification of anything above trivial programs takes years for PhD programmers. There has never even existed a large program (say, more than 200k LoC) that has been formally verified. The most complex formally verified programs I know of are the microkernel SeL4 (~9000 lines of code, excluding the proofs/specs) and CompCert, which I'm still trying to figure out the size of.