Oh, so I have used formal methods for many years (and have written about them [1]), including proof assistants, and have never found that constructive logic in

Oh, so I have used formal methods for many years (and have written about them [1]), including proof assistants, and have never found that constructive logic in general and type theory in particular makes proofs of program correctness any easier. The Curry-Howard correspondence is a cute observation (and it is at the core of Agda), but it's not really practically useful as far as proving algorithm correctness is concerned. [1]: https://pron.github.io https://pron.github.io