4 ms·

If you really want to program mathematics, look at Coq, Agda or Idris.

• 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 ago
    It'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...