106 ms·

> Is it possible to have a programming language where the compiler does the formal verification? Such compiler would require solving halting problem. Most prob

by h91wka 7y ago

> Is it possible to have a programming language where the compiler does the formal verification? Such compiler would require solving halting problem. Most problems related to search of formal proofs are undecidable.

MaxBarraclough 7y ago
This is true, but SPARK and ZZ do it anyway. Automatic deductive program-verification can work, but the halting problem means there will always be truths than cannot be automatically proved. This can still be good enough to get the job done. In the case of SPARK, it's necessary to use timeouts on the prover. Ugly, sure enough, but real work can still be done with it. https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....
- simiones 7y ago
  If we want to go to extremes, it's even worse than the halting problem. Godel's incompleteness theorem shows that, assuming your system is consistent, there are truths that don't have a proof at all, which is even worse than not being able to compute that proof. Still, the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility.
  - MaxBarraclough 7y ago
    > the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility. This is a consequence of the state of current tooling, rather than an inescapable consequence of the relevant math. A concrete example: the SPARK language is a subset of Ada, but with each release it gets less claustrophobic. You can even go to the other end of the programming language spectrum, and use formal methods with functional programming languages. I don't think anyone develops real critical systems this way, but I believe it's an active area of research.
    - simiones 7y ago
      It depends on what kind of guarantees you want, and how much you rely on the language versus programming style. But I think there are fundamental reasons that would prevent you from doing development in full Common Lisp and expect a formal verifier to statically check your code for complex properties (such as halting, bounded memory), and expect it to never reject a correct program. Even with functional languages, the stronger properties you want to check, the more restricted the program must be. For example, Idris can ensure your program halts, but it requires you to write your program in a specific way that can be checked for halting, you can't just take any halting program and expect it to pass the halting checks. Similarly, Rust's borrow checker can verify if your program is free of data races and memory leaks, but you must write your program following specific patterns, even if you can produce data-race and memory leak-free programs in other ways as well (of course, there is the `unsafe` block in Rust exactly for this reason). Of course, there will likely be more improvements as time goes on, but the halting problem puts a fundamental limit on how expressive a language can be while also being amenable to (computable) proof of certain complex properties.
      - steveklabnik 7y ago
        (Rust does not prove the absence of memory leaks)
    - pron 7y ago
      > This is a consequence of the state of current tooling, rather than an inescapable consequence of the relevant math. It actually is an inescapable consequence except that it's far worse than limited languages: limiting languages doesn't help. In fact, langugage is kind of a red herring here. If a language has nothing more than boolean variables and non-recursive non-first-class subroutines, or, alternatively loops up to depth 2 -- it is already beyond our general verification power, as the cost of proving properties grows exponentially in the size of the program, and that kind of language is well below anything usable; usable languages require exponential space and super-exponential time even if they're completely decidable. It's important to remember that the problem isn't a binary distinction between decidable and undecidable. Almost all decidable problems are also impossible. They can take any length of time except infinite. In fact, undecidable problems are a very extreme and exceptional kind of impossible; most impossible computational problems are decidable. See my post here for some results: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity Rather, what formal method do is try to get a certain mix of confidence, difficulty and scale so that they might be able to check some properties with some confidence in some cases. That is the best we can hope for, and what formal methods in industry use actually do. This is still a lot, but people should understand what the rules of the game are.
wolfgke 7y ago
> Such compiler would require solving halting problem. Wrong: Because of the finite memory instead of an unbounded tape (among other reasons), computers are strictly less expressive than Turing machines.
- tzs 7y ago
  Does the proof that the halting problem is not solvable actually make use of the unboundedness of the tape?
  - wolfgke 7y ago
    Of course it does (implicitly!). Otherwise the number of possible states of the Turing machine T that we want to check whether it halts or not is finite and we just have to "simulate" the program and see whether it terminates or it reaches again a state that it was already in.
    - marcosdumay 7y ago
      How would the "if this program halts then run forever, else halt" algorithm work on a real computer? I imagine it would fail with stack overflow.
  - naasking 7y ago
    Standard proof is a diagonalization, which depends on infinite sequences. That said, the Halting problem on physical computers is still of extremely high computational complexity, which can be just as high a barrier as incomputability.
- h91wka 7y ago
  This technically correct comment would be actually useful, if it linked a fully automated prover, that is capable of proving any property of a program that fits in N bytes. If you remove infinite tape, you go from undecidable to "just" exponentially complex.
  - 7y ago
fpoling 7y ago
Strictly speaking real computers are finite state machines and are trivially decidable from the halting problem point of view. The problem is that it just takes long long time.
- h91wka 7y ago
  This argument has been risen and dismissed in this thread already, no need to repeat.
seb314 7y ago
> Such compiler would require solving halting problem. I don't think so. As long as false-negative results are acceptable. (i.e. it is ok if for some programs no proof if found even though they fulfill the specification) Occasional false-negatives seem perfectly fine for real-world use.
- opnitro 7y ago
  In fact all major type systems work this way.
- deleted 7y ago
  [deleted]
curryhoward 7y ago
Not if the human provides the proofs and the compiler merely checks them (like in Coq, for example).
- h91wka 7y ago
  I specifically mentioned in my post that problems related to _proof search_ are undecidable. Coq's tactics for proof search are unreliable. They rely on timeouts and tend to fail ("omega can't solve this system"). So you're not arguing with my post.
  - curryhoward 7y ago
    The question you were answering was not talking about proof search. It was merely asking whether it was possible to do verification in the same language that the program is written in. And, contrary to your response, it is possible to do verification in the same language as the program is written in. Coq is an example of that. Yes, proof search is undecidable. But that's not what we're talking about in this thread. seL4 isn't verified by proof search. The proofs were provided by humans (with limited automation).
deleted 7y ago
[deleted]

by h91wka 7y ago

MaxBarraclough 7y ago

This is true, but SPARK and ZZ do it anyway. Automatic deductive program-verification can work, but the halting problem means there will always be truths than cannot be automatically proved. This can still be good enough to get the job done. In the case of SPARK, it's necessary to use timeouts on the prover. Ugly, sure enough, but real work can still be done with it. https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....

simiones 7y ago
If we want to go to extremes, it's even worse than the halting problem. Godel's incompleteness theorem shows that, assuming your system is consistent, there are truths that don't have a proof at all, which is even worse than not being able to compute that proof. Still, the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility.
- MaxBarraclough 7y ago
  > the only impact this has in practice is that it tells you languages or programming styles amenable to automatic verification must be very limited in their expresiveness/flexibility. This is a consequence of the state of current tooling, rather than an inescapable consequence of the relevant math. A concrete example: the SPARK language is a subset of Ada, but with each release it gets less claustrophobic. You can even go to the other end of the programming language spectrum, and use formal methods with functional programming languages. I don't think anyone develops real critical systems this way, but I believe it's an active area of research.
  - simiones 7y ago
    It depends on what kind of guarantees you want, and how much you rely on the language versus programming style. But I think there are fundamental reasons that would prevent you from doing development in full Common Lisp and expect a formal verifier to statically check your code for complex properties (such as halting, bounded memory), and expect it to never reject a correct program. Even with functional languages, the stronger properties you want to check, the more restricted the program must be. For example, Idris can ensure your program halts, but it requires you to write your program in a specific way that can be checked for halting, you can't just take any halting program and expect it to pass the halting checks. Similarly, Rust's borrow checker can verify if your program is free of data races and memory leaks, but you must write your program following specific patterns, even if you can produce data-race and memory leak-free programs in other ways as well (of course, there is the `unsafe` block in Rust exactly for this reason). Of course, there will likely be more improvements as time goes on, but the halting problem puts a fundamental limit on how expressive a language can be while also being amenable to (computable) proof of certain complex properties.
    - steveklabnik 7y ago
      (Rust does not prove the absence of memory leaks)
  - pron 7y ago
    > This is a consequence of the state of current tooling, rather than an inescapable consequence of the relevant math. It actually is an inescapable consequence except that it's far worse than limited languages: limiting languages doesn't help. In fact, langugage is kind of a red herring here. If a language has nothing more than boolean variables and non-recursive non-first-class subroutines, or, alternatively loops up to depth 2 -- it is already beyond our general verification power, as the cost of proving properties grows exponentially in the size of the program, and that kind of language is well below anything usable; usable languages require exponential space and super-exponential time even if they're completely decidable. It's important to remember that the problem isn't a binary distinction between decidable and undecidable. Almost all decidable problems are also impossible. They can take any length of time except infinite. In fact, undecidable problems are a very extreme and exceptional kind of impossible; most impossible computational problems are decidable. See my post here for some results: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity Rather, what formal method do is try to get a certain mix of confidence, difficulty and scale so that they might be able to check some properties with some confidence in some cases. That is the best we can hope for, and what formal methods in industry use actually do. This is still a lot, but people should understand what the rules of the game are.

wolfgke 7y ago

> Such compiler would require solving halting problem. Wrong: Because of the finite memory instead of an unbounded tape (among other reasons), computers are strictly less expressive than Turing machines.

tzs 7y ago
Does the proof that the halting problem is not solvable actually make use of the unboundedness of the tape?
- wolfgke 7y ago
  Of course it does (implicitly!). Otherwise the number of possible states of the Turing machine T that we want to check whether it halts or not is finite and we just have to "simulate" the program and see whether it terminates or it reaches again a state that it was already in.
  - marcosdumay 7y ago
    How would the "if this program halts then run forever, else halt" algorithm work on a real computer? I imagine it would fail with stack overflow.
- naasking 7y ago
  Standard proof is a diagonalization, which depends on infinite sequences. That said, the Halting problem on physical computers is still of extremely high computational complexity, which can be just as high a barrier as incomputability.
h91wka 7y ago
This technically correct comment would be actually useful, if it linked a fully automated prover, that is capable of proving any property of a program that fits in N bytes. If you remove infinite tape, you go from undecidable to "just" exponentially complex.
- 7y ago

fpoling 7y ago

Strictly speaking real computers are finite state machines and are trivially decidable from the halting problem point of view. The problem is that it just takes long long time.

h91wka 7y ago
This argument has been risen and dismissed in this thread already, no need to repeat.

seb314 7y ago

> Such compiler would require solving halting problem. I don't think so. As long as false-negative results are acceptable. (i.e. it is ok if for some programs no proof if found even though they fulfill the specification) Occasional false-negatives seem perfectly fine for real-world use.

opnitro 7y ago
In fact all major type systems work this way.
deleted 7y ago
[deleted]

curryhoward 7y ago

Not if the human provides the proofs and the compiler merely checks them (like in Coq, for example).

h91wka 7y ago
I specifically mentioned in my post that problems related to _proof search_ are undecidable. Coq's tactics for proof search are unreliable. They rely on timeouts and tend to fail ("omega can't solve this system"). So you're not arguing with my post.
- curryhoward 7y ago
  The question you were answering was not talking about proof search. It was merely asking whether it was possible to do verification in the same language that the program is written in. And, contrary to your response, it is possible to do verification in the same language as the program is written in. Coq is an example of that. Yes, proof search is undecidable. But that's not what we're talking about in this thread. seL4 isn't verified by proof search. The proofs were provided by humans (with limited automation).

deleted 7y ago

[deleted]