3 ms·

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

This is a facetious comment that others have made: https://twitter.com/pigworker/status/913454521610842114 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 7y ago
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 7y ago
  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.
  - ukj 7y ago
    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
  - joycian 7y ago
    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 7y ago
    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 https://ncatlab.org/nlab/show/propositions+as+types
davesmith1983 7y ago
Thanks for explaining what I was trying to say much better than myself.

ukj 7y ago

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 7y ago
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.
- ukj 7y ago
  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
- joycian 7y ago
  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 7y ago
  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 https://ncatlab.org/nlab/show/propositions+as+types

davesmith1983 7y ago

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