Not necessarily, I only argue for utility. You can find better justification in the Curry-Howard correspondence.

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)?