[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.

[joycian]

If it has been proven from your axioms (really down from the axioms!) then you can add it to a library of statements you 'know' (or in the case of your axioms, assume) to be true.

[ukj]

More succinctly: The thing you want proven is a proposition.

A proposition is a type. Writing the algorithm which implements the type is the same as proving it.

https://ncatlab.org/nlab/show/propositions+as+types

[ukj]

A theorem is a consequence of a set of axioms. By definition.

It may be an a-priori truth in the context of the particular proof you are working on, but a-priori your theorem there is always an axiom.

Wanting to prove that X is a theorem of a-priori truth Y is the same thing as writing the algorithm for f: Y -> X

[davesmith1983]

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