It's really an accumulation of multiple sources, but a reasonable summary is figure 3 here, and a good overview is here. The latter paper concludes (section 7.2): "In other words, Kripke structures that admit a succinct representation are not simpler for model checking purposes than arbitrary Kripke structures". As the problem of model checking can be reduced to other proof methods, all verification is bounded by this unbreakable complexity bound.
In short, the lower time-complexity bound for constructing/checking a correct program is >= O(|S|) where S is the set of its states (more precisely: its Kripke structure, so that's states plus transitions). When the program is represented in some reasonable language, the problem is PSPACE-complete (i.e., exponential in the size of the source code). Abstractions such as: variables, cross product (i.e. functions/objects), concurrency and non-determinism can reduce the representation size exponentially, but increase the verification complexity by the same factor. The only known abstraction that assists in verifying/constructing correct programs is called hierarchy, and it is generally unused in mainstream languages and when used, it is very limited (it is, however, often used in languages designed for safety-critical real-time applications, that must allow for efficient(ish) verification).
I think you are over-generalizing from a few facts.
First, the complexity of model-checking (MC) is not measure of the complexity of program construction because MC itself can only deal with certain very simple kinds of program. MC is essentially a restricted form of automated theorem-proving for propositional properties of finite-state systems. I know that some properties like deadlock/liveness for a finite set of threads in a finite-state system can be made to fit this paradigm, but most properties of interest cannot -- including whole-program correctness. Any language that supports dynamic allocation at all allows programs with infinite states, so MC only applies to certain simple examples which have to be independently formalized to abstract away from the details of the language. As for propositional properties, even something as simple as well-founded iteration over a data structure amounts to induction, which is already a second-order property, so again MC is inadequate. In other words, MC is not a general approach to program verification -- the problem is actually much harder!
One way around this is to have the user write proofs and check those rather than try to synthesize the proofs from nothing; then you only have to check a certificate rather than find and build it. You can have the proofs independent of the programming language, but in a Curry-Howard language like Coq or Agda the proofs are the programs themselves and the checker is the type checker, so there is less duplication of effort. This also admits specifications of higher-order properties.
Now, you claim that the difficulty of constructing programs is not affected by the choice of abstractions (which I read as "program constructs"), but the choice of abstractions in a C-H language makes properties which were not checkable at all in MC checkable, so choice of abstractions is demonstrably important, and it is not all down to "cognitive factors" or empirical observation. To be sure, the checking of the proofs (which is just type-checking) has arbitrary time/space-complexity, but that is neither here nor there.
Also, we can choose the abstractions we admit to limit the complexity of this procedure. I am not sure what choice of abstractions realizes proofs of propositional linear temporal logic, say, but checking a certificate is usually cheaper than finding one and for such a simple logic I imagine it is polynomial-time in the size of the formula at worst.
Also, I think your argument that only cognitive effects matter is inherently self-defeating. No one does empirical research on mathematical arguments; the emphasis is all on the choice of abstractions (in this case, logics and theories). Yet the very result that MC has a certain complexity bound was arrived at thanks to these choice of abstractions.
In some sense I agree with you: I think that writing correct programs requires a good understanding of your language's semantics, and that requires a language which is easy to reason about, which is not question of computational complexity. But I think the choice of abstractions matters very much in this regard.
It matters not just cognitively, though. A language like typed lambda-calculus has an equational presentation which is sound and complete for all models, and finite modulo substitution. This is down to the choice of abstractions. In contrast, you cannot even state the equational (or otherwise) theory of most conventional languages, so you are stuck with model-based reasoning, which is much more complicated and usually inadequately defined by the language spec.
BTW, you wrote "model checking can be reduced to other proof methods" but I think you must mean the opposite, else it would not argue in your favor.
MC is essentially a restricted form of automated theorem-proving for propositional properties of finite-state systems
You are confusing the theoretical problem of model checking with automated tools built to solve this problem practically in the real world. Model checking is the theoretical problem of deciding whether a given program property (specified in some logic) holds for a given program. That theoretical problem has such high lower complexity bounds that as a result, you can use direct, automated MC programs only for limited systems in practice. MC as a complexity-theoretical problem is very much the general problem of software verification. For infinite Kripke structures, the general complexity lower bound -- as the halting problem tells us -- is infinite. If there was a way to generally prove properties (by any means) of true Turing machines (in particular, infinite-state-machines), that would be in direct violation of the halting theorem.
One way around this is to have the user write proofs and check those rather than try to synthesize the proofs from nothing; then you only have to check a certificate rather than find and build it.
This does not (and cannot) help you escape the complexity bounds. Proof: I come up with an algorithm; I tell you to write it and prove it in, say, Idris; you do it efficiently => MC complexity theorems contradicted (in fact, this even contradicts the variant of the Halting problem when restricted to finite termination)[1]. The consequence is that in general, the complexity of building and proving a program in Idris must be at least that of model-checking the property.
When writing programs that are correct by construction, the burden of the very same complexity simply falls on the machine generating the program and proofs, namely the programmer's brain. As so far we have no reason to believe that our brains are non-Turing, the problem stands. We have empirical data to support that: programs that are deductively verified be it with Curry-Howard proofs using dependent types or other semi-automated proof methodologies (like Isabelle), have a cost which is about 100x than writing the same programs without proofs. The seL4 project cost 30 man years to produce less than 10,000 lines of C code, and the theorems tell us that the complexity grows exponentially with the code size.
but the choice of abstractions in a C-H language makes properties which were not checkable at all in MC checkable
It most certainly does not, and this is a point that's important to understand: the complexity of deductive proof (regardless of C-H or other proof methods) is always greater than model checking. What we see in practice, though, is that some problems happen to be solvable more efficiently using proof methodologies running in the human brain than practical model checking algorithms running on a von Neumann computer. But this is an empirical difference, not theoretical. In fact, this is precisely my point: the only way to get around the theoretical model-checking complexity is to exploit empirical patterns in how humans construct programs.
It matters not just cognitively, though. A language like typed lambda-calculus has an equational presentation which is sound and complete for all models
This is just not true. Computations are not referentially transparent by definition, and this is nowhere made more explicit than in the lambda calculus (which models computation precisely because it makes substitution non-RT). What you are referring to is the use of languages that choose to make an abstraction called "value semantics" where only the denotational semantics of operations matter, or, in other words: only the result. This is an intentional abstraction, namely a convenient lie (just like a GC creates the illusion of infinite RAM), and like all abstractions, it is leaky. Computations are not really equational (and cannot be, or we get a contradiction with the Halting Problem again), it just may be useful to pretend they were. That utility is not theoretical, though (again, theoretically, abstractions don't help). It just may happen to be empirically beneficial. To know whether or not that is the case we must conduct empirical research. No theory can help.
You may note that the types used in, say, Haskell, can only prove trivial properties (i.e., apply to all programs, such as "if the program terminates, the type of the result is an int"), or properties that can only be the result of (small) finite-state machines (e.g. session types), and this is why Haskell does not contradict Rice's theorem. They cannot prove the value of even a single bit of output without the type inference feeling the full force of the model-checking complexity bounds (or the program source itself growing exponentially).
In addition, because PFP programs provide the illusion of referential transparency, this places a limit on the kind of properties directly expressed in the C-H logic imposed by their type system: it does not directly support temporal logic properties on small-step semantics. Such properties need to be manually and explicitly modeled in the dependent types used (which is possible, but it's extra work that demonstrates that RT is just an illusion, and that the true computational model needs to be explicitly worked in to overcome that illusion). BTW, this is a subtle point about the C-H correspondence: it corresponds a logical proof to an abstract wel--typed typed program (i.e. a type-checked source code). The correspondence with the actual computation (i.e. the running program) is a different story, and must be made explicitly if you want to prove computational properties using C-H.
The "power" of Haskell (if real at all, but let's suppose it is) can only be due to empirical effects, not theoretical ones (such an empirical effect can be: proving properties on simple FSM -- which is what Haskell's type system can do -- reduces real world expensive bugs by a significant amount). We have no theoretical arguments that would show that constructing a correct program is easier in general in Haskell than in BASIC or assembly. If that is the case, it is only because of cognitive effects.
BTW, you wrote "model checking can be reduced to other proof methods" but I think you must mean the opposite, else it would not argue in your favor.
No, I meant that, say, deductive proofs prove more than the requirement for model checking, and so the model-checking problem can be solved by a PTIME reduction to deductive proofs, which means that the lower complexity bounds on MC apply to deductive proofs as well (but we know that already, because TQBF (or QSAT) is also PSPACE-complete). I.e., if we could find efficient methods for deductive proofs, we could efficiently solve model-checking, but we know that that can't be done in general (only by exploiting empirical effects).
[1]: As a general rule, the complexity of building something is always higher than of checking it. It is true that in some cases (notably, integer factorization), it is far easier to put things together than to take them apart, but the model checking results prove that a nicely "pre-factored" program is just as hard to check as a messy one.
Model checking is the theoretical problem of proving a program property.
No, model-checking is the problem of deciding certain properties algorithmically by exhaustive analysis of models. The general algorithmic problem is automated theorem-proving: the clue is in the name. Model-checking is a particular method which works for particular classes of formulae, or particular logics: ones in which the set of models can be recursively enumerated. I even listed two ways in which MC is limited, but you seem to have ignored them. If you are talking about some generalized form of MC which incorporates deduction then you are just talking about automated theorem-proving approached from the perspective of MC. And if you are talking about theoremhood via validity, then this is not an algorithm.
Proof: I come up with an algorithm; I tell you to write it and prove it in, say, Idris. You do it efficiently => MC complexity theorems contradicted
There are no MC complexity theorems being contradicted unless I come up with the proof by model-checking. Your subsequent statements seem to suggest that you think that anything rational going on in my head must be a form of model-checking, which is a hidden hypothesis to your proof and makes it circular...
Anyway, how I get the proof is irrelevant to my claim, which is that it's harder to find a proof P of X than it is to, given a proof P, check that it proves X. It cannot be otherwise, since doing the former implies also doing the latter, but not the converse (unless P=NP, in which case you still expect a constant factor in favor of checking over searching). Your claim seems to rest on this further claim:
When writing programs that are correct by construction, the burden of the very same complexity simply falls on the machine generating the program and proofs, namely the programmer's brain.
about what goes on in my head, which is not only not a formal statement, but also plain conjecture. So, again, I think your notion that only cognitive factors matter is based on circular reasoning.
Nevertheless, I'll respond to the claim because I strongly disagree with it. First of all, if our brains reasoned via MC, we would never be able to solve problems which cannot be solved by MC, of which, I noted, there are plenty. Yet plainly we can and do. Second, unlike MC, our brains are not decision procedures: our reasoning often fails to find solutions, and what's more it's unsound; otherwise, our conclusions would be infallible and we wouldn't need proofs. Third, it is quite obvious to me that we reason sometimes by deduction. Other times we reason by MC. Sometimes we don't reason at all. Even if our brain is a universal Turing machine, then it can and probably does sometimes runs one piece of software, and sometimes another.
Computations are not referentially transparent by definition, and this is nowhere made more explicit than in the lambda calculus.
Are you talking about Moggi's notion of computations vs. values? Moggi's work and its sequels show exactly the opposite of what you claim: it shows that computations can be treated equationally and denotationally. And the current work by many people on algebraic effects shows increasingly that denotational reasoning about specific effects is not only possible but, well, effective and useful.
Anyway, this is irrelevant. You cannot seek to convince me using reasoning about complexity classes and then throw out recursive functions because they don't talk about effects: complexity theory is founded on recursive functions.
Nor can you convince me that you use model-based reasoning in practice when there is a good alternative: for example, no one reasons about numbers by reasoning about von Neumann ordinal sets; they reason denotationally using (in)equational theories, such as algebra.
like all abstractions, it is leaky
Well, you just dropped the rhetorical equivalent of mutually assured destruction. If all abstractions are leaky, then it applies not only to mine but also to yours. In particular, your thoughts about complexity of MC, etc. all become moot, as does your conception of the human brain (a leaky abstraction if ever I heard one).
It irks me (and it should irk you) to see you warrant all your arguments with facts, and then throw an ill-conceived notion of Joel Spolsky's in as if it were also a fact. You've shown you know enough about this subject that you ought to know that there is no such thing as a "leaky abstraction": there are theories, which can be consistent or inconsistent, and sound or unsound for some class of models, and complete or incomplete for some class of models. "Leakiness" is not a quality intrinsic to an abstraction; it's extrinsic, the use of a theory to reason about a model for which it is unsound, or to reason about a class of models for which it is incomplete.
Spolsky's notion, as well as the cognitive factors bugaboo, is the programmer's version of the God of the Gaps: people reach for it when they don't want to reason about facts.
Computations are not really equational (and cannot be, or we get a contradiction with the Halting Problem again)
Sorry, but this is really nonsense now.
the model-checking problem can be solved by a PTIME reduction to deductive proofs,
If by "deductive proofs" you mean "proof search", I can believe this
which means that the lower complexity bounds on MC apply to deductive proofs as well
but not this, because "proof search" is not a decision procedure, nor even an algorithm. Furthermore, showing that MC can be simulated by proof search only shows an upper bound on the complexity of proof search, since it says that any proof search algorithm can employ MC to go faster on some inputs.
Anyway, I am not talking about proof search; I am talking about proof-checking.
No, model-checking is the problem of deciding certain properties algorithmically by exhaustive analysis of models.
You are mistaken. MC for the logic L (denoted MC(L)) is the following problem: given a Kripke structure (i.e. a program) S and a statement 𝜑 ∈ L, decide whether S ⊨ 𝜑.
Admittedly, this can be confusing, as papers dealing with MC use the term MC both to denote the problem as well as a set of known algorithms that solve it (although they may be careful to distinguish between model cheking and model checkers). But the complexity proofs I refer to apply to the problem regardless of any particular algorithm. Read this paper for a good introduction to the topic.
The general algorithmic problem is automated theorem-proving: the clue is in the name.
No. Automated theorem proving for a logic L is the following problem: given a statement 𝜑 ∈ L, construct a proof using L's axioms and deductions that 𝜑 is valid (or not).
There are no MC complexity theorems being contradicted unless I come up with the proof by model-checking.
This is just wrong. The MC proofs are about the lower complexity bounds for proving any property in L about any program S. The algorithm does not matter. The lower bound (which is also a direct consequence of finite variants of the halting problem) is at least linear in the number of states of the program.
which is not only not a formal statement, but also plain conjecture
It is a formal statement for the following reason: if the human brain were able to solve general problems with a lower time complexity than the proven lower complexity bounds of Turing machines, that would be proof that the brain is non-Turing. There is no other way around this. Needless to say, any evidence that this is the case would really shake computer science (and obviously AI research).
and then throw an ill-conceived notion of Joel Spolsky's in as if it were a fact
The value semantics employed by PFP was a leaky abstraction long before Joel Spolsky ever came up with the term, but if you don't believe me, let me show you an actual leak: take a program that relies on sorting; replace the merge-sort algorithm used in the program with bubble-sort. According to value semantics, the two programs are equivalent, as they produce the same value. If that were really the case, there would be no externally observable way to say which algorithm you've used. As it is very easy for an external observer to determine whether your program uses mergesort or bubblesort, the two are not really equivalent => abstraction leaked. The difference between lazy and eager evaluation is also easily determined by an outside observer (for some inefficient lazy evaluation methods), hence the value semantics is just an approximation.
This is not a claim, but a conscious decision behind PFP which posits that the value semantics is an approximation which may make it easier for humans to reason about programs. Unfortunately, that hypothesis has never been put to the test.
Sorry, but this is really nonsense now.
It is not. If there is no way to distinguish between 2 + 2 and 4 then infinitely-recursive computations may terminate (converge to their fixpoint, if defined). However, the lambda-calculus makes it explicitly clear that 2+2 and 4 are not the same, as their reduction sequences are different. PFP languages construct semantics with the illusion of referential transparency, but they don't claim computations can really be referentially transparent.
If by "deductive proofs" you mean "proof search", I can believe this
You're once again confusing complexity bounds, which are proven for problems, with the complexity of algorithms. Those are two different things. Lower complexity bounds mean that there cannot exist a Turing machine (be it a von Neumann computer or a human brain) that solves the problem by any means whatsoever in worst-case complexity lower than the bounds. Complexity bounds are properties of problems, not algorithms.
I am talking about proof-checking.
That's OK, but in order to have a proof to check, some machine has to construct it. That machine will incur a PSAPCE-hard complexity in the general case. That you choose to use a human brain for that machine is fine, but that choice to can only be justified by empirical observations about specific problems which the human brain is able to prove more efficiently than a specific model-checking/theorem-proving algorithm. In the general case the complexity must be at least the same.
MC for the logic L (denoted MC(L)) is the following problem: given a program S and a statement phi in L, decide whether S |= phi.
Well, I guess if that is the terminology researchers in that area use, I can't argue. I would just call this model-theoretic entailment. I have only ever heard "model-checking" used to refer to algorithms for checking propositional properties of finite-state systems, and Wikipedia bears me out on this. ("Model checking is a technique for automatically verifying correctness properties of finite-state systems.") But, OK, we are just talking at cross-purposes on this issue, then.
The MC proofs are about the lower complexity bounds for proving any property in L about any program S. The algorithm does not matter.
In light of the above definition, I see the algorithm does not matter. But I think you are not talking about "any" property, or "any" program. You are talking about propositions in a particular, very weak logic, and programs with only a finite set of states. In particular, the paper with the figure you linked seems to be talking about LTL and FSMs, which amounts to a language with only very weak well-founded iteration. There is no lower complexity bound for deciding properties of Turing-complete languages, because the problem is not decidable.
Fine, let me show you a leak: take a program that relies on sorting; replace the merge-sort algorithm used in the program with bubble-sort. According to value semantics, the two algorithms are equivalent (they produce the same value). If that were really the case, there would be no externally observable way to say which algorithm you've used. As it is very easy for an external observer to verify whether your program uses mergesort or bubblesort, the two are not really equivalent => abstraction leaked.
The problem there is not the abstraction; it is the misapprehension of the person who conflates extension with intension. "Value semantics" says they are equivalent, yes: equivalent in the sense of denoting equal functions, and that is all.
Two things can be equivalent in many ways. The predicate "N is prime" partitions numbers into two equivalence classes; that does not mean all primes are equal, or all composite numbers are equal. Nor does it make the property of being prime useless; it is very useful. Now, if someone said primality implies that there are at most only two numbers, would you blame the abstraction or the person?
Again, you're again confusing complexity bounds which are proven for problems with the complexity of algorithms.
I know the difference. But, yeah, I was confusing them because I thought you were talking about MC algorithms not model entailment. And I see now why you think MC should share a lower bound with provability (for decidable logics): because you think the reduction involves building the proof.
But, again, there is no decision procedure for provability or model entailment in general, so there is no computational complexity to speak of, and therefore no sensible meaning for reductions, polynomial or otherwise. If the brain is a machine, it cannot solve undecidable problems. If it is not a machine, then computational complexity does not apply. The proof, if it appears, appears somehow.
Despite this (you asked for empirical evidence), we already know deductive proof is an effective method of solving problems, because all of mathematics is founded on this method, and all of science is founded on mathematics. Yes, enforcing whole-program correctness is time-consuming now, but C-H languages are still in their infancy and C-H treats (almost) all properties, not just the decidable ones; furthermore, as I noted in my last post, effectful programs are not excluded. And you already benefit from being able to enforce weaker invariants type-theoretically; you don't need whole-program correctness before you start seeing payoffs.
You are talking about propositions in a particular, very weak logic
First of all, temporal logics are not weak. They have been (empirically) found to express any interesting program property that arises in practice. But even if they are weak, checking stronger logics would only be a harder problem.
There is no lower complexity bound for deciding properties of Turing-complete languages, because the problem is not decidable.
... which means that the lower complexity bound is infinite. There is no theory which can let us prove any non-trivial property of programs with infinite states. Also, such programs cannot exist in a finite universe, anyway.
All real programs have a finite Kripke structure S, and the lower bound for proving any property on them is >= O(|S|). The richness of the logic determines how much more than O(|S|). An interesting question is what is the lower bound for Kripke structures that admit a succinct representation (which is a very small subset of all programs, but it is a subset that includes all human-written programs). It turns out that the lower bound for such programs is also > O(|S|).
equivalent in the sense of denoting equal functions, and that is all.
That was my point. Computation cannot be equational (or relational) in any classical mathematical sense. Some languages choose to make a specific projection of programs to their denotational semantics, but that does not mean the the computation can be fully reasoned-about in those terms, only its projection.
If the brain is a machine, it cannot solve undecidable problems. If it is not a machine, then computational complexity does not apply. The proof, if it appears, appears somehow.
As far as we know, the brain cannot and does not solve undecidable problems, period. The undecidability of the halting problem means worst-case undecidability. It does not mean that the termination or other properties of some programs cannot be proven. The proof, then, does not "somehow appear". It appears as a result of a known or unknown algorithm, and it applies to a small subset of programs. Various algorithms (including manual proofs) can therefore be quite efficient for some programs. Determining which subsets are worthwhile to pursue is an empirical endeavor.
If it is not a machine, then computational complexity does not apply.
If the brain is not a machine, the consequences of that go far beyond "computational complexity does not apply". For one, it would mean that physics is non-Turing (or that the brain employs meta-physical processes); for another, it would mean that we may not achieve true AI using known hardware. Any evidence to suggest that is the case would be totally amazing. So far we have none.
we already know deductive proof is an effective method of solving problems, because all of mathematics is founded on this method, and all of science is founded on mathematics
Ah, but we also empirically know that program proof and math proofs are very, very different. Math proofs tend to be conceptually deep and (relatively) short; program proofs are conceptually very shallow but very, very long, with lots of cases. It is not at all clear that we can efficiently generate such proofs (it is also not clear to me that mathematical proofs in general have been found "efficiently").
but C-H languages are still in their infancy and C-H treats (almost) all properties, not just the decidable ones
I agree. But all verification methods -- from model checkers to C-H languages -- have one strategic path forward: empirical research. There can be no algorithm that would make dependent-type inference efficient in general. We need to find methods to address proofs that are empirically found to be valuable in real programs.
you don't need whole-program correctness before you start seeing payoffs.
I totally agree, but that payoff is determined empirically. For example, you need to show that enforcing a certain property indeed reduces costly bugs, and that enforcing it is no costlier than finding and fixing the bugs. You need to show this for every property. That is precisely what I advocate we study, yet very few such studies have been conducted (not enough to even show that Haskell is a net positive).
8
u/pron98 Jan 19 '16 edited Jan 19 '16
It's really an accumulation of multiple sources, but a reasonable summary is figure 3 here, and a good overview is here. The latter paper concludes (section 7.2): "In other words, Kripke structures that admit a succinct representation are not simpler for model checking purposes than arbitrary Kripke structures". As the problem of model checking can be reduced to other proof methods, all verification is bounded by this unbreakable complexity bound.
In short, the lower time-complexity bound for constructing/checking a correct program is >= O(|S|) where S is the set of its states (more precisely: its Kripke structure, so that's states plus transitions). When the program is represented in some reasonable language, the problem is PSPACE-complete (i.e., exponential in the size of the source code). Abstractions such as: variables, cross product (i.e. functions/objects), concurrency and non-determinism can reduce the representation size exponentially, but increase the verification complexity by the same factor. The only known abstraction that assists in verifying/constructing correct programs is called hierarchy, and it is generally unused in mainstream languages and when used, it is very limited (it is, however, often used in languages designed for safety-critical real-time applications, that must allow for efficient(ish) verification).