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-cod...

[1] https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....

Right, 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.