Similarly, many programmers go their entire careers without touching assembly language or logic gates, yet we all know that our programs can be (and are) distil

Similarly, many programmers go their entire careers without touching assembly language or logic gates, yet we all know that our programs can be (and are) distilled down to this. There are definitely people that worry about this, e.g. compiler writers and mathematical logicians, but to most of us it just isn't that important. In addition, it's an abstraction that leaks fairly infrequently, and so far we haven't observed it in the way you're implying; the most prominent "leaks" of mathematical logic are likely unprovability or having to accept stronger axioms to prove a particular statement (e.g. Choice or maybe Grothendieck-Tarski). Addendum: the above is mostly tangential to the original article. The author is very correct that a modern mathematical proof exists, and is formulated to, show another person with suitable background how to work out the truth of a statement. But don't let this form of proof distract you from the existence of the foundations of rigorous proof in general; just as we don't let Ruby's English-like syntax convince us that we aren't truly executing computation. The foundations of mathematical logic are complex, like the transistors on a microchip, but they do "work," in the strongest epistemological sense of the word.