Programming Languages, lambda calculus, calculus of constructions

"Languages like F#, Scala and Haskell each fall somewhere in between these two extremes. None of them are precise enough to accept only halting programs (although Haskell is inching more and more toward a dependently-typed language every year). Yet all of them are more precise than (say) Scheme, where fallible human convention alone determines whether or not the “+” function returns an integer or a chicken."

There's some material for xkcd.com

Reading the rest of the article, one thing I don't get is why the focus on the idea that "programs and proofs are equivalent". You can do math in isolation, but your programs have to run on something which runs on something which runs on something all the way down to the hardware level where at any step along the way you lose control of the "precision" of the code being run or some anomaly environmental/hardware factor affects the overall outcome and the proof is out the window.