Weakening Cycles So That Turing Can Halt

Re:Weakening Cycles So That Turing Can Halt by infogulch on Friday May 15, 2020 @08:47PM (#23199338)

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

[ Parent | on HN ]

Re:Weakening Cycles So That Turing Can Halt by infogulch on Monday May 18, 2020 @09:55PM (#23230556)

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

[ Parent | on HN ]