4 ms·

> In theory, your software itself provides the proof that it does what it claims. If you manage to solve the halting problem first.

seethedeaduu 2y ago
People keep summoning the halting problem in unrelated contexts to handwave things awayvas impossible.
- coldtea 2y ago
  Except in this case, where it's 100% fitting.
  - auggierose 2y ago
    It is only fitting if you think of providing the proof as a push button technology. That makes as much sense as thinking of providing the software itself as a push button technology.
    - coldtea 2y ago
      It has nothing to do with the proof as a push button technology. Adding annotations to the code for example is not a workaround for the halting problem. (Working with a subset that's not-turing complete is, but that doesn't cover the general case the parent calls for, and is not practical with current software development languages and practices).
      - auggierose 2y ago
        Not sure if we are talking about the same thing. If you know why your software is correct, you can write that down as a proof (if you have a language which allows you to do that). If you don't know why your software is correct, well, maybe you should not ship it, because maybe it isn't correct. So yes, it is all about push button technology here. If you are willing to put in the work to write down the proof yourself, instead of expecting a magical entity to generate it for you, then it is possible. All the halting problem says is that there is no such magical entity. You will need to know why your software is correct.
      - adrianN 2y ago
        The halting problem is a worst case statement. For almost all functions a programmer encounters in their job it is trivial to solve.
        Thiez 2y ago
        Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination. A loop where you don't have these things is almost certainly a bug. The vast majority of loops iterate over some finite collection of elements and are thus guaranteed to terminate. Tricky cases are stuff like "I will repeat this operation until the output stops changing".
        coldtea 2y ago
        >Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination. If you're making Space Shuttle software from scratch yes. In practice for 99% of current mainstream development you depend on piles upon piles of dependencies, which might or might not check those loop invariants correctly, or might have a (trivial to add) endless blocking timeout, a deadlock, and many other wonderful things. Usually they're not even set in stone, you'll update to the next version, and if they introduced such an issue, there's lots of fun to be had. Nobody doubted you can have formal proofs for algorithms, or checked software in certain conditions and for certain controlled environments (e.g. using MISRA C and such) (in fact, I support this in a comment elsewhere in this thread). The objection is to the idea that this is applicable (or trivially applicable, and we just aren't doing it out of laziness or something) to regular software development.
  - ulbu 2y ago
    how?
ffsm8 2y ago
That doesn't need to be solved. Continuing the stream of inputs holds no meaning once you've tested every possible permutation (branch coverage) beyond checking for memory leaks. Every software has a finite amount of states it can hold, most developers just erroneously expect some states to be unlikely or impossible to reach.
adrianN 2y ago
The calculations you do to make sure that the bridge doesn’t collapse also require that the steel matched whatever properties your formula assumes. That doesn’t make the calculations useless.
pyrale 2y ago
The halting problem is not an actual issue. It’s a darling of computer science classes, but is you need to prove that your program halts, it’s not that hard to write it in a language subset that is not turing-complete.
auggierose 2y ago
No, you just need to require that somebody who writes the software, also knows why the software halts, and documents the reason properly.
riku_iki 2y ago
> If you manage to solve the halting problem first. there is a large slice of algorithms, which are possible to prove that they are not affected by halting problem. I think having tooling for this slice of algorithms is already a big win.

seethedeaduu 2y ago

People keep summoning the halting problem in unrelated contexts to handwave things awayvas impossible.

coldtea 2y ago
Except in this case, where it's 100% fitting.
- auggierose 2y ago
  It is only fitting if you think of providing the proof as a push button technology. That makes as much sense as thinking of providing the software itself as a push button technology.
  - coldtea 2y ago
    It has nothing to do with the proof as a push button technology. Adding annotations to the code for example is not a workaround for the halting problem. (Working with a subset that's not-turing complete is, but that doesn't cover the general case the parent calls for, and is not practical with current software development languages and practices).
    - auggierose 2y ago
      Not sure if we are talking about the same thing. If you know why your software is correct, you can write that down as a proof (if you have a language which allows you to do that). If you don't know why your software is correct, well, maybe you should not ship it, because maybe it isn't correct. So yes, it is all about push button technology here. If you are willing to put in the work to write down the proof yourself, instead of expecting a magical entity to generate it for you, then it is possible. All the halting problem says is that there is no such magical entity. You will need to know why your software is correct.
    - adrianN 2y ago
      The halting problem is a worst case statement. For almost all functions a programmer encounters in their job it is trivial to solve.
      - Thiez 2y ago
        Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination. A loop where you don't have these things is almost certainly a bug. The vast majority of loops iterate over some finite collection of elements and are thus guaranteed to terminate. Tricky cases are stuff like "I will repeat this operation until the output stops changing".
        coldtea 2y ago
        >Exactly. In practice you always want each loop iteration to perform some action that brings you closer to some desired end state. That loop invariant + some notion of getting closer to the end is usually the proof you need to prove termination. If you're making Space Shuttle software from scratch yes. In practice for 99% of current mainstream development you depend on piles upon piles of dependencies, which might or might not check those loop invariants correctly, or might have a (trivial to add) endless blocking timeout, a deadlock, and many other wonderful things. Usually they're not even set in stone, you'll update to the next version, and if they introduced such an issue, there's lots of fun to be had. Nobody doubted you can have formal proofs for algorithms, or checked software in certain conditions and for certain controlled environments (e.g. using MISRA C and such) (in fact, I support this in a comment elsewhere in this thread). The objection is to the idea that this is applicable (or trivially applicable, and we just aren't doing it out of laziness or something) to regular software development.
- ulbu 2y ago
  how?

ffsm8 2y ago

That doesn't need to be solved. Continuing the stream of inputs holds no meaning once you've tested every possible permutation (branch coverage) beyond checking for memory leaks. Every software has a finite amount of states it can hold, most developers just erroneously expect some states to be unlikely or impossible to reach.

adrianN 2y ago

The calculations you do to make sure that the bridge doesn’t collapse also require that the steel matched whatever properties your formula assumes. That doesn’t make the calculations useless.

pyrale 2y ago

The halting problem is not an actual issue. It’s a darling of computer science classes, but is you need to prove that your program halts, it’s not that hard to write it in a language subset that is not turing-complete.

auggierose 2y ago

No, you just need to require that somebody who writes the software, also knows why the software halts, and documents the reason properly.

riku_iki 2y ago

> If you manage to solve the halting problem first. there is a large slice of algorithms, which are possible to prove that they are not affected by halting problem. I think having tooling for this slice of algorithms is already a big win.