It'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 nev

It'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....