How have you used the Curry Howard correspondence to make proving the correctness of non-trivial algorithms easier (than, say, Isabelle/HOL or TLA+ proofs)?
I hardly use automated formal methods. Disappointing, I know. I use it for thinking through C and Labview programs. It helps with recognizing patterns in data structures and reasoning through code.
For example, malloc returns either null or a pointer. That is an "or" type, but C can't represent that. I use an if statement to decide which (or-elimination), and then call exit() in case of a null. exit() returns an empty type, but C can't represent that properly (maybe a Noreturn function attribute). I wrap all of this in my own malloc_or_error function, and I conclude that it will only return a valid pointer.
Instead of automating a correctness proof in a different language, I run it in my own head. I can make mistakes, but it still helps me write better code.
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.
For example, malloc returns either null or a pointer. That is an "or" type, but C can't represent that. I use an if statement to decide which (or-elimination), and then call exit() in case of a null. exit() returns an empty type, but C can't represent that properly (maybe a Noreturn function attribute). I wrap all of this in my own malloc_or_error function, and I conclude that it will only return a valid pointer.
Instead of automating a correctness proof in a different language, I run it in my own head. I can make mistakes, but it still helps me write better code.