> Unfortunately, unless you're careful, or have a test suite to make sure, it is the case.
Respectfully, you are definitely conflating these concepts. First, a test suite can't replace a model checker. These are two very different things. You can absolutely miss things in a test suite, and even get 100% branch coverage. Your tests can appear to be perfect, and can even pass code review, and still miss things. A test suite can't make sure of anything, because this would imply that your software and your test suite is perfect.
Unit testing is empirical. Not model driven or constructive. Hence, you don't actually have any indication about when you are done. Even if you get to 100% branch coverage. Even if your tests appear to be perfect. You have likely missed tests that exercise cases in your code that you don't even realize are there. Undefined behavior due to integer overflow is common, and almost every mature code base that I have seen -- including SQLite -- misses these classes of errors.
A model checker or a constructive proof system starts from a priori theory. This is used to extract software, or in the case of a source level model checker, the software is used to create the model. While it is certainly possible for gaps to exist here, it's far less likely. Furthermore, there is a direct way to translate this a priori knowledge into "done". If the model checker uses the same libraries as the code generator in the compiler, then there can be a 1:1 relationship between the constructed model and the generated code. Barring inaccuracies in hardware simulation or actual hardware errors or compiler errors, the two will be quite close. If the compiler were extracted from constructive proofs (e.g. CompCert), then the likelihood of compiler errors generating different machine code is even further removed. While nothing is perfect, we are talking about two to three orders of magnitude of added precision over hand-written unit tests.
> You might have a good model, but if your software doesn't actually implement the model...
Ah... there's part of the problem. You don't seem to understand what a model checker is. A model checker transforms source code into a constraint solver, following the same rules that the compiler uses to generate machine code. Yes, there are high-level model checkers that can work on algorithms, but as is clear from the context, I'm talking about source level model checkers. The software and the model are the same. The model is based on the same abstract machine model used for the language and for the particular machine code implementation. The software is transformed into a constraint solver on top of this model. If the two don't match, then a lot of things have gone seriously wrong. In practice, this is about as likely as your compiler generating the wrong code, or your CPU deciding that the MOV instruction really means JMP.
> Not at all. I know the differences.
Clearly not, and here's why:
> Ten years of work for four people, I think... That's a 2000% overhead.
The seL4 team used constructive proof assistant (i.e. Isabelle HOL). Not a model checker (e.g. CBMC). You're conflating the two. You don't understand the difference, and you're plunging ahead as if you do. That is where the crux of this disagreement comes from. Model checkers and constructive proof assistants are both ways to do formal methods, but they are different, with different use cases. seL4 is an atypical example, which used pure constructive proofs because they needed to prove that their operating system implemented well founded process isolation.
When I mentioned that the seL4 team used a model checker, I meant and implied, IN ADDITION TO the constructive proof assistant. This is because both systems are best used for different domains. In practice, the use of a model checker requires relatively minimal overhead. In practice -- my use case -- this is around 30%.
Respectfully, I think you should spend some time studying and using these tools. They will improve the quality of the software you write.
Respectfully, you are definitely conflating these concepts. First, a test suite can't replace a model checker. These are two very different things. You can absolutely miss things in a test suite, and even get 100% branch coverage. Your tests can appear to be perfect, and can even pass code review, and still miss things. A test suite can't make sure of anything, because this would imply that your software and your test suite is perfect.
Unit testing is empirical. Not model driven or constructive. Hence, you don't actually have any indication about when you are done. Even if you get to 100% branch coverage. Even if your tests appear to be perfect. You have likely missed tests that exercise cases in your code that you don't even realize are there. Undefined behavior due to integer overflow is common, and almost every mature code base that I have seen -- including SQLite -- misses these classes of errors.
A model checker or a constructive proof system starts from a priori theory. This is used to extract software, or in the case of a source level model checker, the software is used to create the model. While it is certainly possible for gaps to exist here, it's far less likely. Furthermore, there is a direct way to translate this a priori knowledge into "done". If the model checker uses the same libraries as the code generator in the compiler, then there can be a 1:1 relationship between the constructed model and the generated code. Barring inaccuracies in hardware simulation or actual hardware errors or compiler errors, the two will be quite close. If the compiler were extracted from constructive proofs (e.g. CompCert), then the likelihood of compiler errors generating different machine code is even further removed. While nothing is perfect, we are talking about two to three orders of magnitude of added precision over hand-written unit tests.
> You might have a good model, but if your software doesn't actually implement the model...
Ah... there's part of the problem. You don't seem to understand what a model checker is. A model checker transforms source code into a constraint solver, following the same rules that the compiler uses to generate machine code. Yes, there are high-level model checkers that can work on algorithms, but as is clear from the context, I'm talking about source level model checkers. The software and the model are the same. The model is based on the same abstract machine model used for the language and for the particular machine code implementation. The software is transformed into a constraint solver on top of this model. If the two don't match, then a lot of things have gone seriously wrong. In practice, this is about as likely as your compiler generating the wrong code, or your CPU deciding that the MOV instruction really means JMP.
> Not at all. I know the differences.
Clearly not, and here's why:
> Ten years of work for four people, I think... That's a 2000% overhead.
The seL4 team used constructive proof assistant (i.e. Isabelle HOL). Not a model checker (e.g. CBMC). You're conflating the two. You don't understand the difference, and you're plunging ahead as if you do. That is where the crux of this disagreement comes from. Model checkers and constructive proof assistants are both ways to do formal methods, but they are different, with different use cases. seL4 is an atypical example, which used pure constructive proofs because they needed to prove that their operating system implemented well founded process isolation.
When I mentioned that the seL4 team used a model checker, I meant and implied, IN ADDITION TO the constructive proof assistant. This is because both systems are best used for different domains. In practice, the use of a model checker requires relatively minimal overhead. In practice -- my use case -- this is around 30%.
Respectfully, I think you should spend some time studying and using these tools. They will improve the quality of the software you write.