News for hackers. Stuff that matters.

A comment on Problems of Traditional Math Notation (2004).

Re:Problems of Traditional Math Notation (2004) by adamnemecek on Sunday November 05, 2017 @11:42PM (#15633481)
The main problem with mathematics is the lack of types.
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by mcphage on Monday November 06, 2017 @12:37AM (#15633628)
It has types—it has tons of types. They're just used very differently than in programming.
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by adamnemecek on Monday November 06, 2017 @12:51AM (#15633666)
Which is a problem tho.
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by mcphage on Monday November 06, 2017 @11:04AM (#15636374)
What do you see as the problems with that?
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by adamnemecek on Monday November 06, 2017 @11:42AM (#15636671)
Lack of checkability which slows down progress. Look into work of the late Vladimir Voevodsky https://www.quantamagazine.org/univalent-foundations-redefin...
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by dvhh on Monday November 06, 2017 @02:05AM (#15633841)
it would be so much better if they used Rust
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by adamnemecek on Monday November 06, 2017 @02:21AM (#15633893)
More like coq
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by gnulinux on Monday November 06, 2017 @10:42AM (#15636212)
Coq is intuitionistic, classical proofs cannot be expressed. Mathematicians almost always (unless intuitionistic math is your niche) use classical proofs.
[ Parent | on HN ]
Re:Problems of Traditional Math Notation (2004) by adamnemecek on Monday November 06, 2017 @11:41AM (#15636658)
It kinda is yes. I don’t understand why classical proofs are still a thing.
[ Parent | on HN ]