As someone who's used to functional programming but not familiar with any proof systems, I've sometimes applied Curry-Howard the other way and used Haskell as a primitive proof system by writing the corresponding function (being careful to avoid infinite recursion). GHC's support for "typed holes" makes this pretty convenient - just write a part of the function and leave a hole (_) for the rest, GHC tells you what type is needed there.