1. 7

  2. 2

    I saw this talk when first learning Haskell, but it didn’t really “click” for me until I started using the coq proof assistant. Every program you write is converts “evidence” of one or more propositions into “evidence” of the proposition that you want to prove. I recommend spending a bit of time with the jscoq version of the Software Foundations book!