Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec...
by chriswarbo on Saturday September 22, 2018 @12:18AM
(#18044423)
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.
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.