3 ms·

But why do I have to accept your arbitrary program? Why couldn't I only consider programs that come with a proof that they terminate? I don't care how you mad

But why do I have to accept your arbitrary program? Why couldn't I only consider programs that come with a proof that they terminate? I don't care how you made the proof, maybe you used some restrictive programming language that can only express concepts that terminate, or your program implements paxos and you prove it by some embedding into Coq. Some restrictions though: the proof has to be formulated in a way that's compact and takes linear-time to check [1], and the proof goes down to some formalization of first-order logic that we can agree on. [1]: Yes, I think this is possible. [2] [2]: https://github.com/digama0/mm0#introduction https://github.com/digama0/mm0#introduction

infogulch 6y ago
After a bit of searching, proof carrying code seems to be related to what I'm describing [3]. So I guess my point is: Does it really matter that you can come up with arbitrary programs that I will be unable to determine if they halt, if I can build up an entire OS platform of provably correct machine code with correctness proofs that I can scan out of a file to verify? Ultimately, here's the point of re-framing it like this in the first place: Now it's just a tooling problem. I recognize that this is a very big 'just'. [3] https://people.eecs.berkeley.edu/~necula/pcc.html https://people.eecs.berkeley.edu/~necula/pcc.html