Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec...
by gnulinux on Thursday September 20, 2018 @10:51PM
(#18036871)
This is such a shallow comment, very surprising its up there. (Did I miss a joke?)
Mathematics is written in a language that is not only precise enough to make it easier to follow logical arguments, but also optimized for human readability. Mysql is written in C, which is optimized in the early days of computing for portability between machines, which is an irrelevant goal to provability. C does not give enough guarantees to prove anything worthwhile, whereas the language of mathematics has been evolving since the 19th century to give as much guarantees as possible. If mysql would be written in agda, it'd be so much more easier to prove it compared to Wiles' proof of Fermat's or whatever. As far as any programming language go, C is probably the worst language you can prove anything let alone mysql.
OP comment wasn't implying proving is supposed to be easy. Mathematics is not written for machines, it's written for humans. Ultimately, the act of writing mathematical papers is not that much different than act of writing sociology papers. A mathematical proof is written so that it convinces a human. Once you start writing those proofs into Coq or agda or whatever, you start seeing how much handwaving is going in mathematics. This is because being experienced in mathematics gives one the ability and confidence to operate on higher levels of abstraction which doesn't need as much precision/rigor as a programming language as context signals the tactic, argument etc...
Mathematics is written in a language that is not only precise enough to make it easier to follow logical arguments, but also optimized for human readability. Mysql is written in C, which is optimized in the early days of computing for portability between machines, which is an irrelevant goal to provability. C does not give enough guarantees to prove anything worthwhile, whereas the language of mathematics has been evolving since the 19th century to give as much guarantees as possible. If mysql would be written in agda, it'd be so much more easier to prove it compared to Wiles' proof of Fermat's or whatever. As far as any programming language go, C is probably the worst language you can prove anything let alone mysql.
OP comment wasn't implying proving is supposed to be easy. Mathematics is not written for machines, it's written for humans. Ultimately, the act of writing mathematical papers is not that much different than act of writing sociology papers. A mathematical proof is written so that it convinces a human. Once you start writing those proofs into Coq or agda or whatever, you start seeing how much handwaving is going in mathematics. This is because being experienced in mathematics gives one the ability and confidence to operate on higher levels of abstraction which doesn't need as much precision/rigor as a programming language as context signals the tactic, argument etc...