Comment by pron
1 day ago
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.
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.