3 ms·
> In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. But programming is a subse
by godelski 4mo ago
> In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof.
But programming is a subset of mathematics. They are both formal languages. I suspect the trustworthiness is more in your comfort level than the ability to verify
- zmgsabst 4mo agoThat depends on who you ask. Type theory can also be an independent synthetic foundation atop which you build mathematics.
- godelski 4mo agoYou can build all of mathematics on type theory? I very much doubt that considering there isn't even a fully unified mathematics. There's holes that don't know how to be bridged between entire subfields. So I'd be impressed if type theory really could do everything, but hey, I don't know