News for hackers. Stuff that matters.
Re:On rebooting: the unreasonable effectiveness of turning c... by mkleczek on Wednesday May 25, 2022 @04:04AM (#31501774)
> Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties.

Translated: there exists a computational model weaker than TM but strong enough to implement programs we care about.

Unfortunately, we don't know such computational model and we know empirically surprisingly many problems require a TM (ie. surprisingly many languages are accidentally Turing complete)

Re:On rebooting: the unreasonable effectiveness of turning c... by ncmncm on Wednesday May 25, 2022 @04:56AM (#31502037)
Making a system Turing-complete, even accidentally, does not make it proof against analysis. A system or input for the system may be built out of parts that could be used to make an undecidable system. But that does not mean you can only build undecidable systems with those parts.

It is in fact extremely common to build wholly deterministic machines out of the same parts as our unreliable computers, that are correct by construction. And they may implement a Turing-complete language and still be wholly deterministic, just by limiting the input to what can be proven deterministic in a strictly limited time. Again, this is normally by construction, where the proof is always trivial.

Such a proven-correct system can model literally any space-constrained algorithm.

Re:On rebooting: the unreasonable effectiveness of turning c... by mkleczek on Wednesday May 25, 2022 @05:38AM (#31502284)
> It is in fact extremely common to build wholly deterministic machines out of the same parts as our unreliable computers, that are correct by construction.

It is neither common nor easy but actually provably impossible. Please read this piece carefully: https://pron.github.io/posts/correctness-and-complexity

Re:On rebooting: the unreasonable effectiveness of turning c... by ncmncm on Wednesday May 25, 2022 @06:42AM (#31502629)
Yet, it is done, thousands of times every day, all over the world.

You must be misunderstanding the work if you believe that what is being done routinely is impossible.

Re:On rebooting: the unreasonable effectiveness of turning c... by mkleczek on Wednesday May 25, 2022 @07:03AM (#31502777)
> You must be misunderstanding the work if you believe that what is being done routinely is impossible.

Quite possibly I don't understand what you mean by "work". If by "work" you mean creating provably correct software then no, it is not done routinely.

Re:On rebooting: the unreasonable effectiveness of turning c... by ncmncm on Wednesday May 25, 2022 @07:27AM (#31502988)
The work is the paper you cited.

People create wholly deterministic state machines all the damn time.

Re:On rebooting: the unreasonable effectiveness of turning c... by mkleczek on Wednesday May 25, 2022 @07:50AM (#31503198)
> People create wholly deterministic state machines all the damn time.

What do you mean by "wholly deterministic"?

Re:On rebooting: the unreasonable effectiveness of turning c... by ncmncm on Wednesday May 25, 2022 @01:44PM (#31507918)
All possible states are well-understood, all possible paths through states are mapped.

You can buy an 8-bit adder/accumulator from a catalog.

Re:On rebooting: the unreasonable effectiveness of turning c... by librexpr on Wednesday May 25, 2022 @04:23AM (#31501872)
I just want to point out that you don't need to know the precise bounds of such a computational model to prove things about your programs. There already exist Turing-complete programming languages where you can prove non-trivial properties about your program and which have had practical applications, for example F* and its use in Project Everest.

https://project-everest.github.io/

https://www.fstar-lang.org/

Re:On rebooting: the unreasonable effectiveness of turning c... by mkleczek on Wednesday May 25, 2022 @05:31AM (#31502239)
Just having a language that allows you to prove things does not mean it is possible to prove them.

We still don't know if it is possible to build a provably correct multi-tasking OS or a web browser without security vulnerabilities. If it was easy we would already have one written in FStar or Idris.

While admiring all the work done by Project Everest - the fact is that it is a multi-year project (I first read about it about 3-4 years ago and it was already under way) with a very limited scope - it is more of an evidence of difficulties of writing correct software.