4 ms·
The main problem with mathematics is the lack of types.
by adamnemecek 9y ago
The main problem with mathematics is the lack of types.
- mcphage 9y agoIt has types—it has tons of types. They're just used very differently than in programming.
- adamnemecek 9y agoWhich is a problem tho.
- mcphage 9y agoWhat do you see as the problems with that?
- adamnemecek 9y agoLack of checkability which slows down progress. Look into work of the late Vladimir Voevodsky https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/ https://www.quantamagazine.org/univalent-foundations-redefin...
- dvhh 9y agoit would be so much better if they used Rust
- adamnemecek 9y agoMore like coq
- gnulinux 9y agoCoq is intuitionistic, classical proofs cannot be expressed. Mathematicians almost always (unless intuitionistic math is your niche) use classical proofs.
- adamnemecek 9y agoIt kinda is yes. I don’t understand why classical proofs are still a thing.