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 a

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.