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.