[howardcurry]

This is a facetious comment that others have made: https://twitter.com/pigworker/status/913454521610842114

One issue that it glosses over is that in mathematics, the object of study is a-priori truths (and mathematicians are usually Platonists). I would express this as saying that math is interested in knowing what's true. So obviously it is applicable to proving things about programs. So far so good.

But programming involves a lot of work which could be described as a-posteriori. As an example on dictionary.com puts it, "an a posteriori argument [...] derives the theory from the evidence". Programmers are designers, wrestling sense out of complex and sometimes poorly expressed specifications, requirements, and realities. This doesn't map onto mathematics: it's neither (in Gowers' terms) theory building nor problem solving, because mathematical theory building is an a-priori business dealing reflexively with mathematical tools, not with theories of the outside reality. A typical large software system is an unwieldy, organic thing, to which mathematically formulated theories apply in the same way as they do to biological organisms. Sometimes math can describe aspects a complex system well, but it can't tell you how to build it, any more than it can tell you how to build the Parthenon.

[ukj]

A-priori truths are called axioms.

In the context of the Curry-Howard isomorphism you don't "prove things about programs".

Programs ARE proofs. Not all programs, mind you. You need to be using a dependently-typed language like Agda, Coq or Idris.

The link in my post to the UniMath project is a bunch of codified proofs to various theorems in Category theory, Topology, Combinatorics etc.

[howardcurry]

I don't agree that a-priori truths are limited to axioms—it's a much larger category of "necessary" truths. A theorem which has been proved is an a-priori truth.

Sure, programs are proofs in the context of Curry-Howard. But not necessarily proofs of what you want them to prove.

[davesmith1983]

Thanks for explaining what I was trying to say much better than myself.