> The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs).
If we accept that a software program is isomorphic to a proof, is there anything that isn't isomorphic with a proof?
I can prove Pythogoras' theorem with a diagram, so by extension anything in the physical world is a manifestation of mathematical theory and, since it exists, is isomorphic with a trivial proof for something.
I'm inclined to agree with you; though the key word here is "trivial".
Types are propositions, and programs are proofs of their types. Unfortunately most programs are overly-complicated proofs of trivial propositions (when looked at from the mathematical side of curry-howard; of course what's actually the case is that we tend to only use types to specify a tiny part of what our programs are meant to do).
In an untyped language every expression has the same type (which we might call `Thing`, and contains integers, strings, functions, etc.) so in the curry-howard sense every expression is proof of the same trivial proposition.
I'm inclined to think of the laws of physics (whatever they are) as a programming language, and physical systems as programs running in that language. On first impression, it doesn't seem like physics is typed; hence every physical system is a proof of a trivial proposition (essentially: physical things can exist). It would be interesting to hear a counterargument though.
Note that in these cases it's the types/propositions which are trivial, not necessarily the programs/proofs. Consider that we could, if we wanted, prove a pretty trivial proposition like `((A -> B) AND A) -> B` in a roundabout way that involved applications of Fermat's last theorem. I tend to call such things "(over)complicated", rather than "complext", since their complexity isn't inherent or required.
I don't think I agree with this statement. As a matter of fact, I've always had a deep unease with so-called "geometric proofs", where a succession of visual transformations of a diagram are used to prove a theorem.
You can certain explain the intuition behind the proof of Pythagoras theorem with a diagram, and there's huge pedagogic value in doing that.
But to me it isn't a formal proof until it has been codified in a language that a computer can walk from start to end making sure each step is valid.
scratches head I'm pretty sure I can come up with a codified language proof that you will accept, then define a mapping between the language and transformations of a diagram. And while not an expert on isomorphism, but I'm pretty sure that makes the visual proof isomorphic with the codified language and hence valid (and, indeed, computable).
Basically, although code and proofs are in a sense isomorphic, I think everything and proofs are isomorpic in the same sense. So claiming that proofs should be structured to the same standards as code because code is isomorphic to proof is a bit of a non-sequitur. Why not show the layout of my rock garden is isomorphic to code and hence proving something (my rock garden can be Turing complete) and then claim my rock garden should be structured like a program?
Basically, the idea that the structure mathematicians favour for proofs have fallen behind programmers laying out of code is not well substantiated and the idea that 'proofs are isomorphic to code' is not useful because it is far too broad.
It's not so much that programs are isomorphic to proofs; it's that mathematics and programming are the same activity. It's essentially a historical accident that the people who practice this activity have ended up in different groups, and that those groups use different terminology for the same things ("program" vs "proof", "type" vs "proposition", "execute" vs "simplify", "tuple" vs "conjunction", "union" vs "disjunction", "function" vs "implication", "dependent function" vs "universal quantification", "interface" vs "existential", "programming language" vs "logical system", etc.).
All of the relationships between these are the same too (e.g. a program `p` has type `T`, iff the proof `p` proves the proposition `T`; the proof `w` proves that the existence of `x` implies the proposition `y AND z` iff the program `w` is a function which generates a tuple of `(y, z)` when given an argument implementing the interface `x`; and so on).
Mathematicians and programmers do care about different things. Mathematicians are more concerned with informally proving previously unknown results; which corresponds to something like learning that a type has a value by sketching some pseudocode. Programmers care deeply about how many steps their proofs (programs) take to simplify; how easy it is to modify a proof to prove a slightly different proposition, etc. Yet there are so many good ideas on each side that are immediately applicable (e.g. dependently typed languages take rigorous logical systems and view them as programming languages; proof engineering takes software engineering ideas and applies them to building and maintaining proofs).
I'm struggling to think of an activity involving rock gardens that corresponds precisely to, say, universal quantification.
Of course, that still leaves the same problem of explicit proofs being tedious, i.e. being able to prove pythagoras's theorem "with a diagram" does not mean being able to prove it "within an explicit, formalised diagram language".
If we accept that a software program is isomorphic to a proof, is there anything that isn't isomorphic with a proof?
I can prove Pythogoras' theorem with a diagram, so by extension anything in the physical world is a manifestation of mathematical theory and, since it exists, is isomorphic with a trivial proof for something.