2 ms·

There is still one glaring issue with your thesis that remains unresolved. Verification is hard. We all agree. But that is for the worst case. Alternatively

• pron 10y ago
  > How should I convince myself that it is hard either (1) to verify even programs that are specifically designed to be verified, or (2) to write such programs? Didn't we discuss that issue on Reddit? Anyway, as the complexity of verification is proportional to the number of states. If you write the program from scratch, the number of states is dictated by your spec (as every computational problem, every function has an inherent computational complexity). Your spec can be arbitrarily hard. Now, it's not a matter of worst-case. That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying. Indeed, you can see that static analysis tools can often prove on arbitrary programs the very same properties that are enforced by type systems. Of course, not every algorithm and property are worst-case, regardless of whether the program is being written or given. There are useful classes of programs/properties that are easier to verify, and the language can make useful restrictions. So far, examples that work well in practice are SPARK and SCADE. Each forbids memory allocation, including unrestricted stack growth.
  • tome 10y ago
    > That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying. I don't follow. What has A got to do with it? I am given a spec P. You claim that it's hard to write a program that satisfies P, pretty much regardless of what P is. I don't see how A is relevant at all.
    • pron 10y ago
      Yes, but P can be arbitrarily hard to implement. This is hard for you to see, so I'm incorporating A into P just as an example of how we can make the spec hard. If it were easy to write programs that conform to arbitrary specifications, it would have been just as easy to verify arbitrary programs, because I can reduce the latter to the former by making the arbitrary program the spec of the new one. If you want another example of how a spec can be hard, consider this one: "write a program that for every input n, an even integer greater than two, outputs the smaller of two primes whose sum is n". Do you think writing that program and proving it correct is any easier than verifying the 10-liner in my post? Or even this: "write a program that sorts a list of integers". You know for a fact that that program has a minimal time complexity of O(n lg n). That complexity, in turn, partly determines how hard it will be proving the program correct. You know that it will be easier than "write a program that returns the first element of its input list", whose time complexity is O(1) (actually the difficulty of verification is more related to the space complexity, because the space complexity is a better approximation of the number of states the algorithm must have in order to solve the problem, unless the algorithm can be a pushdown automaton).
      • tome 10y ago
        Sure, I know that there are some specifications P that are hard to implement (and some that are impossible!). What's not clear to me is whether the specifications we care about implementing in practice are hard to implement.
        • pron 10y ago
          In practice it's obvious that they're hard! Look at the bugs people make and look at the effort required for seL4/CompCert (both are fairly simple systems).
          • tome 10y ago
            Ah, but that's not my question! My question is whether the specifications we are interested in implementing in practice are hard in theory.