I did some Googling after reading the article and found this book by Dijkstra and Scholten actually showing how a first-order language could be adapted to yield easy and teachable corectness proofs. That is actually amazing! I have a degree in CS and unfortunately I’ve never seen a formal specification system that could actually be implemented and not be just some almost-tautological mathematical logic, like so many systems that exist in the academia. Thanks very much for the link.
If you are interested in this kind of thing, you should check out Dafny. It’s a programming language with Hoare-logic style pre- and postconditions (and the underlying implementation computes weakest preconditions, Dijkstra-style). But what sets it apart is that it is backed by an automatic theorem prover (Z3) which is sufficiently powerful to handle most things that seem trivial to a human. To me Dafny feels like the promise of programming verification research in the 1970s finally came through: you can carry out program verification like you would with pen and paper, without being overwhelmed by finicky algebraic manipulations.
I did some Googling after reading the article and found this book by Dijkstra and Scholten actually showing how a first-order language could be adapted to yield easy and teachable corectness proofs. That is actually amazing! I have a degree in CS and unfortunately I’ve never seen a formal specification system that could actually be implemented and not be just some almost-tautological mathematical logic, like so many systems that exist in the academia. Thanks very much for the link.
If you are interested in this kind of thing, you should check out Dafny. It’s a programming language with Hoare-logic style pre- and postconditions (and the underlying implementation computes weakest preconditions, Dijkstra-style). But what sets it apart is that it is backed by an automatic theorem prover (Z3) which is sufficiently powerful to handle most things that seem trivial to a human. To me Dafny feels like the promise of programming verification research in the 1970s finally came through: you can carry out program verification like you would with pen and paper, without being overwhelmed by finicky algebraic manipulations.