3 ms·
_Finding_ a proof is undecidable. _Verifying_ that a proof is correct is easy (it's usually linear-ish in the length of the proof). If the programmer supplies
by curtisf 5y ago
_Finding_ a proof is undecidable.
_Verifying_ that a proof is correct is easy (it's usually linear-ish in the length of the proof).
If the programmer supplies (most of) the proof, a compiler can easily certify that the proof is correct with respect to its model of the program.
Still, constraint solvers (often SMT solvers) can succeed a lot of the time (just not _all_ of the time) in automating pieces of proofs, so all the tedium doesn't need to be left with the programmer.
In particular, generally programmers write code that they believe is correct, so if they're right then there's usually a straightforward proof that it is correct since their beliefs will only get so complicated.
- AlexCoventry 5y agoAh, arbitrary heap-allocated structures a human can supply a proof for. Thanks; makes sense.
- sterlind 5y agomy only experience in this area is Dafny, which aggressively automates the proof-finding (by passing it to Z3), but when that fails the compiler is exceedingly vague on what remaining obligations need to be discharged. You have to stumble around in the dark, trying asserts and assumes, until you narrow down where it got stumped. are there other automated-proof languages that do a better job on this?