> 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.
Such compiler would require solving halting problem. Most problems related to search of formal proofs are undecidable.
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....
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.
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.
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.
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
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.
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.
That doesn't matter. I mean, you might be able to prove some properties in this way just as you could in others, but it is not a "solution" by any means -- it might work in some cases for some properties with some barely acceptable scalability, and that's about it. The reason is that the cost of reasoning about n components is not even a computable function of n (the cost grows in the same way if you were trying to prove the property on a monolith). See the blog post I linked to for a result that proved this, and an example of a case where two components are easily analyzed yet their composition isn't.
The main direction in formal methods research to increase scalability in a viable way is to reduce soundness.
AFAIU Component-Based Software Engineering has been a bedrock principle of applied formal verification for decades. It's a process approach. If a functional problem is sufficiently complex it's necessary, if not always sufficient, as a practical matter to use a component architecture. And even if it's not sufficient, a solution where some components are formally verified is better than where none are. Circumscribing soundness isn't an alternative, it's complementary.
You're right, it's not by itself a "solution" in the sense of completely resolving the problem; it's a "solution" in the other meaning of that word--a means of dealing with a problem.
Yes, and still the only software verified using such techniques has been tiny (< 10KLOC) and required extraordinary simplification and tremendous effort by specialists. It's like saying that particle accelerators have been a bedrock principle of turning lead into gold. It "works" but not in any sense that makes it a repeatable, affordable practice. Moreover, the gap between the size of programs verifiable in this way and the size of a "normal" piece of business software has stayed pretty much constant over the past four decades -- 3 orders of magnitude.
> And even if it's not sufficient, a solution where some components are formally verified is better than where none are.
Better in what sense? Is it better to soundly verify one component or to use unsound methods on an entire system (even assuming similar costs, but often the latter is cheaper). Soundness is costly and is never a real requirement as a software system is a physical system, anyway; machines only perform machine instructions according to spec with some probability, and probability is all engineers can ever hope for. But sure, sometimes there are small components that are easy enough to verify with deductive proofs, making it the most affordable path to high confidence, although I'd say that's the rare exception rather than the rule.
> Circumscribing soundness isn't an alternative, it's complementary.
It allows you to use automated methods that don't require careful modularity.
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.
So you're not arguing with my post.
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).
Wrong: Because of the finite memory instead of an unbounded tape (among other reasons), computers are strictly less expressive than Turing machines.
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.
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.
If you remove infinite tape, you go from undecidable to "just" exponentially complex.
Which is a huge leap - we got from "impossible" to "possible in principle" and we now can do research how to make it even "sufficiently fast" for problems of practical relevance.