News for hackers. Stuff that matters.
Re:Will Computers Redefine the Roots of Math? by digama on Wednesday May 20, 2015 @11:45AM (#9577078)
It's already in this state. See Coq-in-Coq, where Coq formalizes its own foundations. Note that this is not entirely convincing, because if Coq was in fact inconsistent then the fact that it could prove its consistency is not surprising. But it is impossible to truly overcome this, and it certainly goes a long way to improve confidence in the system.

There are no comments on this comment yet.