Model checking is great, and many tools developed by the model checking community are marvellous (especially the TLA+ model checker).
But deductive methods scale well enough to definitively establish integrity and confidentiality for an entire OS kernel. They scale well enough to show that that said kernel has no in-kernel storage channels that can be exploited in a side channel attack.
Deductive methods scale well enough to verify (completely automaticallly, without human intervention) that the compiled binaries faithfully implement a given C program, so the compiler and linker need not be trusted.
These are deep properties. You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length (not algorithm sketches or high-level system descriptions, actual code that compiles and runs).
That's for deductive approaches in general. But sone of your specific claims about type theory are dubious as well. Elsewhere you claim that
> The fact that even current formal verification research is mostly looking elsewhere seems to suggest that the answer is likely negative
Your claim that formal methods research is mostly looking elsewhere is really stretching it. More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year. The number of submissions to ICFP's TyDe track had over 30% growth last year. TYPES already dwarfs the biggest conferences devoted to model checking or any other specific formal method. No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere". No other subfields are ezperiencing comparable growth.
Unfortunately, they do not. The two projects you mentioned are positively tiny -- they correspond to about 10KLOC of C, or less than 1/5th the size of jQuery -- and they each took world experts years of effort. Both, BTW, required serious limitations in the algorithms used to keep them simple. That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator.
> You're welcome to give examples of model checking or concolic testing establishing comparably deep properties of actual code of comparable length
Concolic tests are unsound, which is why they scale so well. Model checking routinely verifies much larger codebases, so much so that people don't bothering writing papers about it. When deductive methods are used to verify a 10KLOC program that's news. You can buy off-the-shelf model checkers that do more in industry pretty much all the time.
> More researchers are doing type theory than ever. Grants are pouring in, some labs can offer 20+ PhD scholarships per year.
Perhaps, but when you look at FM conferences, deductive methods in general and type systems in particular are significantly more represented.
> No widely cited research aeticles express the sentiment that "type theory has failed and we should look elsewhere"
There's no need to abandon something that has yet to break through in the first place. Most FM research is just done elsewhere.
> No other subfields are ezperiencing comparable growth.
Automated methods are.
When you establish actual deep properties, that's news. You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker.
Again, if non-deductive formal methods are routinely used to establish comparably deep properties of programs of comparable size (as you claim), you should have no trouble naming at least one example. You don't need research papers to justify that claim, just a few statements of the form "Global Property P of 10k line C Program Q was established by model checker R".
> That's like saying that transmuting lead into gold scales well because we can transmute ten gold atoms in a billion-dollar particle accelerator.
No, not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels. While that is a significant expense, there is no order of magnitude difference, much less something in the "billion dollar particle accelerator" territory. Especially since it delivered global correctness properties that are out of reach for any other method.
Model checkers don't usually beat deductive proofs in both size and depth, but they often easily beat them on any one of these.
In terms of code size, model checkers have verified reachability on C programs of over 50KLOC in less than an hour for at least 15 years now (BLAST). Some bugs found in the past few years Linux kernel with a model checker are here: http://linuxtesting.org/results/ldv-cpachecker
In terms of depth -- there are too many to choose from. Both SCADE and Simulink are routinely used in industry to verify LTL. TLC, a model checker for TLA+ was used to develop and verify deep properties of the OpenComRTOS kernel https://en.wikipedia.org/wiki/OpenComRTOS
> You can't buy any model checker that verifies confidentiality for actual kernels. At all. There is no such model checker.
There is no real method like this of any kind. A heroic effort by teams of PhD candidate proof monkeys working for some years isn't a technique.
> not really. NICTA kept tabs on this, and got that producing seL4 costs about 50% more per line of code than other commercial L4 microkernels.
I don't know what the cost of producing commercial L4 microkernels, but that 10KLOC program took 12 person years, plus another 12 for tooling. 2 years per KLOC, and even half of that, is well beyond the reach of 99% of software, plus no one has ever managed to use deductive verification for programs that are significantly larger than that in any amount of time. That's about three (!) orders of magnitude behind ordinary business software. This gap has remained pretty much constant over the last forty years.
I think it is possible that deductive proofs may become viable in industry in some high-assurance, high-cost domains, provided that the programs are very small. But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
Deductive methods the assembly refinement proof of seL4 (binary verification) is completely automated, and takes less than two hours on a modern PC.
OpenComRTOS is much much smaller and simpler than seL4 (comparable to eChronos). It's important work, and a neat example at how formal modeling allows one to _design better products_ even in well-explored domains, but it's a really poor example for illustrating the supposed scalability of model checking compared to deductive methods. Especially ehen the book on the system emphasizes how they kept experiencing state explosions which broke the checker during development.
In any case, TLC checks specifications, not implementations; it's not appropriate to compare them to deductive methods that work on actual source code (cf. the properties of the _specification_ account for less than 5% of total proof obligations, and establish global properties that are stronger and deeper than model checking could provide). Attempts to use TLA+ on implementations such as C2TLA+ are far less successful, it's not been demonstrated to scale well (no case studies above 1 kloc at all). Writing and checking specifications is useful, and leads to more reliable software, and you're free to argue that there is far more low-hanging fruit to be found in this area than in dependent type systems. But it's not the same as checking 50kloc _programs_, and you should not conflate these activiities.
Not to say that many deductive tools are completely automated and have been shown to work at scale too: SydTV verifies the correspondence between thr seL4 binary and the corresponding sourcr in under two hours on a modern PC.
And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking.
> But there is no sign that it could reasonably be a basis for increasing correctness of more ordinary software.
You're entitled to that opinion. Just don't conflate that with general trends and sentiments in the formal methods community. Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere".
The same goes for your claim that non-deductive techniques scale better and establish deeper properties than deductive ones: if you believe this will be shown decisively true in the future, that's a perfectly alright opinion to have, and you'll find plenty of peiple who share it. But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods.
(ps. Writing these posts took me a lot of time, so I'll have to limit myself to one more comment in this thread.)
TLC checks specifications of arbitrary detail. I don't see why it matters when it comes to deep properties. There does not exist any method -- automated or manual -- that can verify deep properties of code of size even within an order of magnitude of ordinary applications. Inasmuch as model checkers and deductive proofs work at all, model checkers are clearly more scalable.
> But it's not the same as checking 50kloc _programs_, and you should not conflate these activities.
I explicitly said that model checkers don't beat deductive proofs on size and depth at the same time, but they do beat them easily separately. Still, there are a few cases where model checkers fail, and the only option available is formal proof. Usually, that is too expensive, but we have seen that in extreme circumstances when a great amount of work is applied to a very small amount of code, this could "work" in the sense that specialized, highly-trained teams working for a long time could do it. AFAIK, this has so far only been tried in research projects, and never by "ordinary" engineers.
> And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking.
If checking a proof were comparable to finding one, then the P vs NP problem would have been resolved a long time ago. You should compare the time it takes to write and model-check a 3500-line TLA+ spec vs the time it takes to write a 3500 line Agda program and check the proofs.
> Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere".
I didn't say there was consensus; I said that the majority of researchers are looking elsewhere, and that's where most research is focused.
> But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods.
Deductive methods have been studied for at least forty years now, and AFAIK, they have never been used in any meaningful scale by non-researchers in industry. On the other hand, while automated methods obviously have not reached the point that they could automatically verify arbitrary properties of arbitrarily sized code -- and they never will, and neither will deductive methods -- they are being used in industry on a regular basis, with capabilities ranging on depth, scale, and soundness, and their use is growing; just in the safety-critical space where SCADE and Simulink are used, but at Microsoft, Amazon, Oracle and Facebook as well as smaller companies. As an applicable formal method in the real world, deductive proofs don't even exist yet, heroic efforts by researchers notwithstanding.
Which is why it's unsurprising that more researchers are looking into methods that have had some measure of success outside research. I find all aspects of formal methods very interesting, and I wish all researchers luck and success (and I sometimes amuse myself with small machine-checked proofs, usually in the TLA+ proof assistant or sometimes in Lean), but it is misleading to present deductive and automated methods as being on equal footings in terms of real-world success.
I also think there is a fundamental mismatch between deductive proofs and software verification, something I call the "soundness problem." Unlike mathematics, while an algorithm can be proven correct, a software system never can, any more than a chair could -- it's a physical system. This means that soundness is never, ever, ever a requirement in software verification. On the other hand, achieving soundness (for deep properties) is very costly, as both theory and experience tell us. This is why many experiments these days -- both in academia and industry -- try to turn down the soundness knob to achieve other actual requirements in software verification (see O'Hearn's recent "incorrectness logic"). A method that is inflexible on soundness -- which is both not required and very costly, is one that seems to be clashing with the very needs of software verification.
This is also why you find that research projects using deductive proofs are almost invariably done by people with little or no industry experience. They treat the problem of software verification as an academic exercise without understanding what real software is and how it's used. On the other hand, you see many more researchers with industry experience looking into automated methods. It's funny, to see the transformation. You look at someone like Peter O'Hearn that's moved from academia to industry. What does he do then? Turn down soundness. You also see it with Leslie Lamport and David Harel, and I could probably find more examples. Once researchers are faced with how software is actually developed, the first thing they realize you need to do is to reduce soundness (for deep properties). Soundness is not a requirement, and it is the enemy of scale and speed, which are (I've written a short post on one aspect where researchers don't understand how software is written: https://pron.github.io/posts/people-dont-write-programs). There are cases in software where soundness is needed -- automatic refactoring and compiler optimization -- which is why I think type systems are interesting for those, but correctness -- not so much.
On the other hands approaches to correctness based on dependent types are favored by people who may be very good researchers, but are not professional programmers, not familiar with industry, and have not conducted field studies (people like Bob Harper, Adam Chlipala, Edwin Brady, and Leonardo de Moura). Now, their research is very good, but it is theoretical, and so far unsuitable for any field use, which is unsurprising, given that they're unfamiliar with how software is made. Which brings me back to my original point: bringing dependent types to Haskell is an interesting first field experiment, but it is just that -- a research experiment designed to answer a research question (someone who worked on seL4 told me that they believe they could bring the cost down enough to be similar to that of high-assurance software, but that's not where Haskell is or, I think, wants to be). It is very different from the kind of work that people like O'Hearn and Lamport are doing, which is scaling up approaches that have already shown their worth in the field.
better scalability than
deductive
- Scalable to large code bases.
- Scalable to deep properties.
Deductive methods are currently the only ones that scale to deep properties. Model checking et al are currently the much better at scaling to large code bases. Note however two things: First, Facebook's infer tool which scales quite well to large code bases, is partly based on deductive methods. Secondly, and most importantly, under the hood in most current approaches, SAT/SMT solvers do much of the heavy lifting. Existing SAT/SMT solvers are invariably based on DPLL, i.e. resolution, i.e. a deductive method.
Model checkers check deep properties with overall significantly less effort. It is true that they don't always succeed, but neither do deductive proofs. In industry, deductive methods are used as a last resort, when they're used at all, to tie together results from automated techniques.
> Note however two things: ...
That's not what I meant by "deductive methods;" I meant verification by semi-automated deductive proofs. Also, SMT solvers aren't used in isolation to verify significant pieces of software, they're used as components of model checkers, concolic testing and proof assistants (or to verify local properties of code units), so they're used in both semi-automated deductive methods as well as in automated methods. I also believe that DPLL is based on assignment and backtracking, not resolution.
Model checkers check deep
DPLL is based
TLC is a model checker can check most properties expressible in TLA+, which are more expressive than any base lambda-calculus theory (e.g. it includes temporal refinement properties). See my overview on TLA+'s theory: https://pron.github.io/tlaplus
> in real implementations you mostly simply enumerate models, and backtrack (maybe with some learning) if you decided to abandon a specific model
So not deductive. You know that because DPLL does not directly yield a proof of UNSAT.
can check most properties
expressible in TLA+
- Assume we 'measure' the complexity of a property by the number of quantifier alternations in the logical formula.
- Assume we 'measure' the complexity of a program by lines of code.
(Yes, both measures are simplistic.) What is the most complex property that has been established in TLA fully automatically with no hand tweaking etc for more than 50,000 LoCs? And how does that complexity compare to for example the complexity of the formula that has been used in the verification of SeL4?
So not deductive.
There is an interesting question here: what is the precise meaning of "deductive"? Informally it means: building proof trees by instantiating axiom and rule scheme. But that is vague. What does that mean exactly? Are modern SAT/SMT solvers doing this? The field of proof complexity thinks of (propositional) proof systems simply as poly-time functions onto propositional tautologies.
TLC, a model checker for TLA+, is commonly used to verify arbitrary properties -- at least as "deep" as those used in seL4, and often deeper -- of TLA+ specifications of a few thousand lines. Those properties can informally correspond to codebases with hundreds of thousands of lines, but there is currently no method for formally verifying arbitrary properties of 50KLOC, be it automatic or manual. Automated methods, however, are used either for deep properties (quantifier alterations) of few k-lines of spec/code or shallower (though still non-local and non-compositional) properties of 50-100KLOC. Manual deductive methods are virtually used for nothing outside of research projects/teams, except for local, compositional properties, of the kind expressible by simple type systems.
I clarified further here: https://news.ycombinator.com/item?id=22146186
> So first-order logic is not deductive, because it doesn't yield a direct proof of FALSE?
In any logic you can work deductively in the proof theory, or in the model theory. DPLL SAT solvers work in the model theory of first-order logic. Also, SAT solvers work on propositional logic, not first-order logic. Because of completeness, we know that every model-theoretic proof corresponds to a proof-theoretic proof, but that's not how most SAT algorithms work (except for resolution solvers).
> There is an interesting question here: what is the precise meaning of "deductive"?
It means using the syntactic inference rules of a proof theory, rather than the semantic rules of a model theory (possibly relying on completeness meta-theorems, as in the case of propositional logic, although that's not relevant for most interesting first-order theories). SMT solvers employ SAT, and can work on some first-order theories. I am not familiar with all the techniques SMT solvers use, but I believe they employ both proof-theoretic and model-theoretic techniques. In any event, as I mentioned before, SMT solvers are rarely used alone, because they're very limited. They are used as automated helpers for specific steps in proof assistants (TLAPS, the TLA+ proof assistant makes heavy use of SMT solvers for proof steps), for local properties of code (e.g. OpenJML for Java, in Dafny and in SPARK) or as components in CEGAR model checkers and in concolic test systems.
TLC ... is commonly used to ...
at least as "deep" as those
used in seL4, and often deeper
One problem with model-checking is that you handle loops by replacing loops with approximations (unrolling the loop a few times) and in effect only verifying properties that are not affected by such approximations. In other words extremely shallow properties. (You may use different words, like "timeout" or "unsound technique" but from a logical POV, it's all the same ...)
the model theory ...
rather than the semantic
rules of a model theory
With that, what mathematicians call a model is but another deductive theory, e.g. the model theory of Peano Arithmetic happens in ZFC, another deductive theory. The deductive/non-deductive distinction is really a discussion of different kinds of algorithms. Deduction somehow involves building up proof trees from axioms and rules, using unification. It could be fair to say that concrete DPLL implementations (as opposed to textbook presentations) that are based on model enumeration, non-chronological backtracking, random restarts, clause learning, watched literals etc don't quite fit this algorithmic pattern. I am not sure exactly how to delineate deductive from non-deductive algorithms, that's why I think it's an interesting question.
SMT solvers are rarely used alone,
* * *
No, I am not. Read what I wrote again :)
> and please don't forget to collect your Turing Award!
Some people have already beat me to it. The 2007 Turing Award was awarded for the invention of model checkers that precisely and soundly check deep properties.
> One problem with model-checking is that you handle loops by replacing loops with approximations
No, that's what sound static analysis with abstract interpretation does. Model checkers are both sound and precise, i.e. they have neither false positives nor false negatives. To the extent they use sound abstraction (i.e. over-approximation), as in CEGAR algorithms, they do so to increase performance and to sometimes be able to handle infinite state spaces. A model checker, however, is always sound and precise, or else it's not a model checker.
> In other words extremely shallow properties.
Model checkers commonly check arbitrarily deep properties. Engineers in industry use them for this purpose every day.
> All mathematics is deductive.
Yes, and all (or much, depending on your favorite philosophy of mathematics) of it has models. If you have two apples in one hand and one apple in the other and you count how many you have, you have not done so using deduction in any logical theory. That had you used such a process you would have also reached the same result is because of soundness and completeness meta-theorems. That mathematics has both proof and model theories, and that they're compatible, is the most important result in formal logic.
> All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.
All verification methods are limited by both size of code and depth of properties. For non-trivial property, the least scalable method, on average, is deductive proof. Which is not to say it is not useful when automated methods have failed.
Be that as it may, seL4 cannot currently be automatically verified, and it's not due to code size (8700 lines of C and 600 lines of assembler). It's hard to see what the obstacle to mechanisation could be but logical complexity.
Model theory is not some magical deduction-free paradise. The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent. Building models of Peano arithmetic in ZFC for example, but also relating constructive and classical logic through double negation or embedding type theory in set theory, are all about relative consistency. It's easy to make a FOM (= foundation of mathematics) unsound, and logical luminaries including Frege, Church and Martin-Lof managed to do so. Those soundness proofs in essence transform a proof of falsity in one system to the other, and relative consistency is the best we can get in order to increase our confidence in a formal system. It is true that traditional model theory, as for example done in [1, 2, 3]. doesn't really foreground the deductive nature of ZFC, it's taken for granted, and reasoning proceeds at a more informal level. If you want to mechanise those proofs, you will have to go back to deduction.
[1] W. Hodges, Model Theory.
[2] D. Marker, Model Theory: An Introduction.
[3] C. C. Chang, H. J. Keisler Model theory.
There is no impenetrable obstacle if humans could do it (for some definition of "could"), but the difficulty is handling infinite state spaces. Model checkers can do it in some situations, but the could do it in more. Neither model checkers nor humans can handle infinite state spaces -- or even very large ones -- in all situations (halting problem and its generalizations).
> Model theory is not some magical deduction-free paradise.
I just pointed out that some of the most successful automated methods, like model checkers (hence their name, BTW) and SAT solvers (which are really special kinds of model checkers), work in the model, not the proof theory.
> The reason we care about model theory in logic is because we want to have evidence that the deductive system at hand is consistent.
The reason we care about models is that we want to know that the "symbols game" of formal logic corresponds to mathematical objects; i.e. that it is sound -- a stronger property than consistency. The model existed first. Proof theory in deductive systems -- and formal logic in general as we know it -- is a 20th-century invention (well, late 19th but only accepted by mathematicians in the 20th).
I gave an example of increasing correctness in the context of record data types, something almost every business app does.
> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods.
And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query?
> There are easier ways, like Java's permission system, that I mentioned elsewhere.
Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
A tank is a way of getting people to work faster than walking, a concern that almost all people have, but that doesn't mean we should propose tanks for that purpose. That dependent types could increase correctness doesn't mean they should be added to a language -- unless its goal is research. This is a common problem I see. Say A is some business concern. The question we need to answer to decide whether to use solution B is not B => A but A => B.
What you're saying is that if I choose to use technique X and I want to achieve Y, then this is a way to do it. This is not the same as saying this is a good technique of achieving Y. The logical implication is reversed from what we'd like to find out. At best you're saying if you use dependent types, you increase correctness. I want to know what you should do to increase correctness, and using dependent types might be the worst possible option. The question is not whether dependent types imply increased correctness, but whether wanting increased correctness implies we should use dependent types. In fact, the post cites a case study about dependent Haskell that isn't exactly a glowing review of the feature.
> And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query?
"Type-checking a SQL query" is not a business goal, and if I try to convert it to some goal you may have been referring to, for example, what is a good way to check if there are mistakes of some simple class in a SQL query, then I'm not sure simple testing isn't more than sufficient. Having said that, I like simple type systems, and I think they are also sufficient for that (e.g. there are typesafe SQL libraries for Java).
> Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
I don't know what the requirements are so I don't know.
You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever? Should Java not have added lambdas because it already had anonymous inner classes? You can clearly get by just fine in a lot of business applications without some of these features.
I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness. It’s not so clear that dependent types are too complex a solution there, especially if you look at a library like Servant, which already uses some advanced type system features, and which is actually a really practical library that is probably used in production applications as well. A library like Servant might be able to expressed more clearly with dependent types than with a hodgepodge of type system extensions. I think that wanting type-safe REST API access is already an order of magnitude more practical than model checking kernel code.
That's like saying that a tank could get you to work, so some of its uses are practical for civilians. Does the weight of dependent types justify such disproportionate applicability?
> You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever?
And those arguments would be just true, except that industry languages adopted those features many years after they've been tried in research languages and shown their worth, while industry languages didn't adopt other features (or perhaps haven't yet), because they didn't prove to be the right solutions to big problems. It's perfectly fine to adopt many ideas that are open research questions, but if you do so you can't deny that your goal is research.
> I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness.
No, because that's the inverted implication, or "tank" problem again. Just because a tank can get you to work doesn't mean that it should. If you want to achieve goal A, and feature B achieves it, i.e. B => A, you cannot conclude from that that you should adopt B. You're assuming A and B => A and concluding B. That just doesn't follow.
The question we're asking is whether A => B. We're not asking whether dependent types can be put to some practical use -- that's what researchers ask. We engineers ask what solution to our problem we should adopt (usually the least costly one).
So what? Even if you think having X is good, that doesn't mean having 100X is necessarily better.
> Dependant types are a simple and unifying way to solve a variety of shortcomings with conventional statically typed systems.
But solving problems with type systems is not a business goal. Increasing correctness is.
> What alternatives do you have in mind?
The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods. Dependent types are a powerful, general and complex mechanism that only scales well for very simple problems.
> Given the various hugely expensive bugs I have been involved in (e.g. Java toString on a date reading the system locale). I would say yes.
There are easier ways, like Java's permission system, that I mentioned elsewhere.