[pron]

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

[amavect]

I think for a cute observation, the metaphor helps me grasp where I can apply logic. I'll read your blog in my free time, thanks for sharing.