4 ms·
The article shows how interesting properties can be proved (with a nontrivial amount of effort). That's cool, but I wouldn't call it correct by construction.
by atq2119 3y ago
The article shows how interesting properties can be proved (with a nontrivial amount of effort). That's cool, but I wouldn't call it correct by construction.
- MaxBarraclough 3y agoIt's a standard phrase in the formal methods field, [0] emphasising that it's an alternative to the usual approach where we hope that our testing (which can never be complete) is enough to catch all the worrisome bugs. Personally, this article didn't strike me as being very easy to follow, or as being the most compelling demonstration of the value of formal methods. At the risk of going off-topic: if you're not seeing the point, I recommend this example using SPARK, a non-functional language. [1] [0] https://betterprogramming.pub/a-taste-of-coq-and-correct-code-by-construction-111bf74d3b98 https://betterprogramming.pub/a-taste-of-coq-and-correct-cod... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html#proving-spark-programs https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....
- MaxBarraclough 3y ago10 days too late to edit: the first link should have been https://wiki.c2.com/?CorrectByConstruction https://wiki.c2.com/?CorrectByConstruction
- thaliaarchi 3y agoRight, not all of the techniques shown yield code that’s correct by construction. For example, an argument was indirectly given, and that error was only found after writing a theorem involving it and finding it was impossible to prove. In the section “Correct BST by Construction”, they explain the technique of requiring every constructor of a BST to supply a proof that it maintains the properties of a BST. Any modification to a BST constructs a new BST (since Coq is pure), so any operations on a BST must also supply a proof of their correctness. That is correct by construction.