Comment by qsort

If you want to see how the Curry-Howard isomorphism works in practice, this is a very accessible introduction: https://groups.seas.harvard.edu/courses/cs152/2021sp/lecture...