Re:The Anti-Human Consequences of Static Typing
by jeapostrophe on Monday August 12, 2013 @05:16PM
(#6202041)
If you really believe this, you should try to translate any contemporary (published) mathematical proof into a real logic, like Coq. It is hard and people earn PhDs doing this because most proofs are so intuition heavy in the first place.
Re:The Anti-Human Consequences of Static Typing
by freyrs3 on Monday August 12, 2013 @05:31PM
(#6202145)
I have spent several months doing proofs in Coq, as well as in Isabelle. I contest conflating Coq with "real logic", it is perfectly possible to do rigorous proofs without the aid of a computer-aided proof assistant, if that wasn't the case then there wouldn't be any reason to trust the authors of the proof assistant in the first place.
Re:The Anti-Human Consequences of Static Typing
by jeapostrophe on Monday August 12, 2013 @07:21PM
(#6202897)
Certainly, but most math proofs aren't "rigorous proofs" by any stretch.
Mathematical proofs are explicitly logical statements, if they aren't based in logic they aren't proofs by definition. Mathematical intuition is what leads us to ideas but it's only within the framework of formal reasoning that we "know" anything within mathematics. Poincare said it nicely:
"It is by logic we prove, it is by intuition that we invent."