The deep link equating math proofs and computer programs
Okay. Today I&#x27;ll be the idiot.<p>I don&#x27;t get it. Or rather, I don&#x27;t get the significance of the Curry-Howard Isomorphism. Questions:<p>1) Is there an example of a proof and its corresponding program that makes you say &quot;whoa, trippy, I didn&#x27;t expect those to be related&quot;? Like, yeah, an Int -&gt; Boolean function &quot;proves&quot; you can construct a Boolean from an integer, but ... so what? What would a non-trivial proof (say, on the order of the Pons Asinorum) look like as a program?<p>2) Are the &quot;programs&quot; referred to here to merely pure functions (i.e. side effect-free, global state-free ones)? It <i>sounds</i> like it is based on lines like this:<p>&gt;When a computer program runs, each line is “evaluated” to yield a single output.<p>That ... seems to cram  &quot;computer programs&quot; into some kind of Procrustean bed <i>unless</i> we&#x27;re taking about pure functions. But then it also talks about how CHI has applications in verifiable programs, which, I&#x27;m told, <i>can</i> reason about side effects.<p>Feel free to call me an idiot, as long as you can also inspire an aha-moment.