47 ms·
Well, there's a significant difference there. Hilbert seems aimed at computational mathematics more in line with Mathematica rather than the logical foundationa
by tel 12y ago
Well, there's a significant difference there. Hilbert seems aimed at computational mathematics more in line with Mathematica rather than the logical foundational work occurring in Coq/Agda/Idris.
- moomin 12y agoIt'd be nice to achieve both... you wouldn't get some of the silly errors documented elsewhere in the thread. Admittedly, that's way more ambitious than anything anyone's actually implemented, ever...