4 ms·
You can run it, it's just that the operation of the program is not interesting. Voevodsky's system is proof relevant so, at least, the programs themselves are i
by tel 11y ago
You can run it, it's just that the operation of the program is not interesting. Voevodsky's system is proof relevant so, at least, the programs themselves are interesting, but other models exist where the programs aren't even interesting. Their mere existence is all that matters.
- mathgenius 11y agoYes, once you formalize (in computer code) a bit of mathematics you can run it, but i'm pointing out that you don't need to formalize (the correctness of) a program in order to run it. I guess it is not much of a distinction, because a (non-formalized) mathematical argument can also carry "invariants" (like loop invariants in a for-loop) that somehow cross-check its correctness.
- nmrm2 11y agoYou also don't have to prove a theorem in order to use it. To give an elementary example, you can conjecture that a given mapping is something-morphism between two groups and use that morphism to carry out a proof about one group in terms of a known result about the other group. In fact, "conjecture lemma; verify main result is true using the conjectured lemma; go back an prove lemma" is a bog standard problem solving technique in Mathematics... edit: Oh, I see what you mean is bit more nuanced than I understood at first. But this is still true -- often you can probably check that the mapping you've written down is a something-morphism locally, for the elements you're working with atm. I'm stretching the example now, but you get my point? I imagine this is probably not unheard of in research-grade mathematics -- e.g. we don't have a general proof for "really cool conjecture" so we check it in special cases whereever we think it might be useful to have... idk.