4 ms·

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

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.
  - wahern 7y ago
    > as the cost of proving properties grows exponentially in the size of the program Exactly. And the solution is architectural modularization--implementing a solution as multiple components that can each be independently verified and then integrated in a verifiable manner. Microkernels are uniquely amenable to such an approach, regardless of language. Which I think is the major reason why memory allocation in seL4, including memory for in-kernel runtime objects, is handled in user space, otherwise its tentacles would make kernel verification intractable. And it's not just that allocation is handled by a single user space daemon; it bleeds into the entire architecture. AFAIU, any request you make of the kernel must be accompanied by the necessary memory needed to satisfy the request. This also fits nicely into the capability model.
    - 7y ago

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.
- wahern 7y ago
  > as the cost of proving properties grows exponentially in the size of the program Exactly. And the solution is architectural modularization--implementing a solution as multiple components that can each be independently verified and then integrated in a verifiable manner. Microkernels are uniquely amenable to such an approach, regardless of language. Which I think is the major reason why memory allocation in seL4, including memory for in-kernel runtime objects, is handled in user space, otherwise its tentacles would make kernel verification intractable. And it's not just that allocation is handled by a single user space daemon; it bleeds into the entire architecture. AFAIU, any request you make of the kernel must be accompanied by the necessary memory needed to satisfy the request. This also fits nicely into the capability model.
  - 7y ago