3 ms·

> you can prove that arbitrary heap allocated data structures with pointers are bug-free Can you say a bit more about that? The way that's written, it sounds l

• 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 ago
    Ah, arbitrary heap-allocated structures a human can supply a proof for. Thanks; makes sense.
  • sterlind 5y ago
    my 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?