I disagree with the author’s claim that there are no black boxes in mathematics. In fact, this is exactly what lemmas and theorems serve as: a statement (like a typing interface or function signature) together with a proof (a “program”) that satisfies that interface. In large-scale mathematics we rarely unfold every proof; we use those results as black boxes — otherwise the work would be unsustainable.

I also disagree with the broader implication that the languages of programming and mathematics (i.e., logic) are inherently distant. On the contrary, they share deep structural isomorphisms as evidenced by the Curry–Howard correspondence.