3 ms·

Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try. Wikipedia: [1] Turing proved no

Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try. Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cannot be correct. [1] https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem

lmm 6mo ago
And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.
- AnimalMuppet 6mo ago
  Some correct programs are supposed to run forever. When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times. So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself, mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for programs like OSes).
  - Rusky 6mo ago
    This is not actually a problem for total languages, which simply model these kinds of processes using corecursion/coinduction/codata.
  - gopiandcode 6mo ago
    you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/ https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/ https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.
    - DonaldPShimoda 6mo ago
      > finite programs that run on an infinite stream of events This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.
  - hmry 6mo ago
    Two different meanings of "forever" there. An OS runs for an arbitrarily large finite time, which is different from an infinite time. Same way you can count to any finite integer with enough time, but you can never count to infinity. Those kinds of interactive programs take in a stream of input events, which can be arbitrarily long, but eventually ends when the computer is shut down. Termination checkers don't stop you from writing these interactive loops, they only stop non-interactive loops
ashton314 6mo ago
> reasoning about program correctness is not possible Not possible for all problems. We cannot decide correctness (ie adherence to a specification) for all programs, but we can definitely recognize a good chunk of cases (both positive and negative) that are useful. The Halting Problem itself is recognizable. The surprising result of Turing’s work was that we can’t decide it.
mkl 6mo ago
We care only about a very small and narrow subset of possible programs, not any arbitrary one. It's possible to solve this kind of problem in large enough classes of program to be useful.
raincole 6mo ago
> a given arbitrary program and input Keyword emphasis mine.
- grg0 6mo ago
  That one little word that changes everything in how you interpret the statement.
muraiki 6mo ago
When you write a recursive function, Lean’s kernel requires a termination proof, unless the function is a partial or marked as unsafe. In those cases, they can’t be used in proofs. https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#The-Lean-Language-Reference--Definitions--Recursive-Definitions--Well-Founded-Recursion--Termination-proofs https://lean-lang.org/doc/reference/latest/Definitions/Recur...
DonaldPShimoda 6mo ago
> Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. This is so reductive a framing as to be essentially useless [0]. I think maybe you want to learn more about program correctness, formal verification, and programming language semantics before you make such statements in the future. [0] See, e.g., type-checking.

lmm 6mo ago

And Alonzo Church proved in 1940 that you can avoid this problem by using a typed language in which all programs halt. But sadly some programmers still resist this.

AnimalMuppet 6mo ago
Some correct programs are supposed to run forever. When is an OS supposed to halt? When you shut it down, or when you power down the hardware, and no other times. So if you don't do either of those things, then the OS is supposed to run forever. Does that, by itself, mean that the program is incorrect, or that the language is inadequate? No, it means that the definition is worthless (or at least worthless for programs like OSes).
- Rusky 6mo ago
  This is not actually a problem for total languages, which simply model these kinds of processes using corecursion/coinduction/codata.
- gopiandcode 6mo ago
  you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/ https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/ https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.
  - DonaldPShimoda 6mo ago
    > finite programs that run on an infinite stream of events This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.
- hmry 6mo ago
  Two different meanings of "forever" there. An OS runs for an arbitrarily large finite time, which is different from an infinite time. Same way you can count to any finite integer with enough time, but you can never count to infinity. Those kinds of interactive programs take in a stream of input events, which can be arbitrarily long, but eventually ends when the computer is shut down. Termination checkers don't stop you from writing these interactive loops, they only stop non-interactive loops

ashton314 6mo ago

> reasoning about program correctness is not possible Not possible for all problems. We cannot decide correctness (ie adherence to a specification) for all programs, but we can definitely recognize a good chunk of cases (both positive and negative) that are useful. The Halting Problem itself is recognizable. The surprising result of Turing’s work was that we can’t decide it.

mkl 6mo ago

We care only about a very small and narrow subset of possible programs, not any arbitrary one. It's possible to solve this kind of problem in large enough classes of program to be useful.

raincole 6mo ago

> a given arbitrary program and input Keyword emphasis mine.

grg0 6mo ago
That one little word that changes everything in how you interpret the statement.

muraiki 6mo ago

When you write a recursive function, Lean’s kernel requires a termination proof, unless the function is a partial or marked as unsafe. In those cases, they can’t be used in proofs. https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#The-Lean-Language-Reference--Definitions--Recursive-Definitions--Well-Founded-Recursion--Termination-proofs https://lean-lang.org/doc/reference/latest/Definitions/Recur...

DonaldPShimoda 6mo ago

> Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. This is so reductive a framing as to be essentially useless [0]. I think maybe you want to learn more about program correctness, formal verification, and programming language semantics before you make such statements in the future. [0] See, e.g., type-checking.