Comment by Cladode | Hacker News Reader

Comment by Cladode | Hacker News Reader

Parent Full thread

   TLC ... is commonly used to ... 
   at least as "deep" as those 
   used in seL4, and often deeper

What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC. I do not believe that without a demonstration ... and please don't forget to collect your Turing Award!

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

All mathematics is deductive. ZFC is a deductive theory, HOL is a deductive theory, HoTT is a deductive theory. MLTT is a deductive theory, Quine's NF is a deductive 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,

I agree, but model checkers, type checkers for dependent types , modern testing technques, and (interactive) provers all tend to off-load at least parts of their work to SAT/SMT solvers which makes the opposition between deductive and non-deductive methods unclear.

         * * *

BTW I am not arguing against fuzzing, concolic, model checking testing etc. All I'm saying is that they too have scalability limits, just that the scale involved here is not lines of code.

> What you are in essence implying here is that the SeL4 verification can be handled fully automatically by TLC.

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.

Sorry, I got confused about loops in model checking, I was wrong about that. I don't know what happened, since I even have co-authored a model-checking paper where we do check loops.

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.

> It's hard to see what the obstacle to mechanisation could be but logical complexity.

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).

Reply on news.ycombinator.com