1. 7

The original study saying formal verification was useless. In Section 6 of this paper, Avra Cohn gave a similar reality check when attempting to mechanize a hardware proof. Also, Guttman summarizes here problems with many verification efforts. Finally, Wired has a modern take on debate in 1979 paper by de Millo et al. These collectively represent most of opposition’ points to formal verification of software.

  1. 3

    This is great for its description of social process of mathematics, the traditional approaches, and the limitations. I’m probably going to do a takedown of some points in the de Millo et al work at some point because I think the field got far enough to address some of it. There’s still some truth in what they’re saying. Probably best to treat new approaches as something different from traditional math with their own goals and expectations.

    Any rebuttal of mine would focus on the LCF + de Bruijn approach negating much risk in proof steps, the high-level languages/frameworks that were built to make it easier (not easy), the fact that many people are doing what they suggest they won’t, the examples corroborating reliability benefits, and something exploring vetted theorems vs vetted verified components which I think are similar in how they’re used.

    The risk that they predicted best was trusting verified components so much they didn’t include other checks: many ended up doing that. Good news is we have ways to do assurance in depth for those that are willing. Essentially, we just combine different methods of risk mitigation instead of relying on any one too much. Also, always have field updates, monitoring and recovery built into the plan for the system.

    1. 2

      I’d be very interested in this, especially reflecting on the automated verification that’s become possible since this paper was written.

      1. 1

        Thanks. It will probably be something I do a little over time, esp as I learn the stuff hands-on. The automated stuff was certainly a counterpoint. Nothing that handles full correctness past simple stuff has been totally automated that I’m aware of given there’s always stuff the SAT/SMT solvers have trouble with.

        On small systems, esp in embedded, that’s gotten over 90% of the proof obligations in a lot of projects, though. On specific properties that are important, we have lots of automation that can handle them. Both type systems and sound static analysis are examples. The full correctness has scaled up to filesystems, compilers, and OS kernels. Static analyzers checking specific properties have scaled up to the Linux kernel. Individual pieces that we’d need to know were correct to support static analyzers’ claims have themselves been verified to full correctness in isolation. Further, the accounting programs they mentioned are mostly decimal or floating point computations. The glider done in SPARK automated floating-point fairly well.

        So, those are some counters with real-world evidence to some of their claims in the area of whether proof would be useful, on what systems, and with what level of confidence. Also, that there’s industrial programmers using SPARK, Coq, Isabelle/HOL, ACL2, and esp Design-by-Contract every day refutes the claim nobody would do it or check it. Matter of fact, Design-by-Contract lets one cheat to use proofs or runtime checks depending on time/complexity involved. If using latter, it can handle arbitrary-sized programs with reduced guarantee that they’ll work or fail-safe taking you to point of failure.

        At that point, it’s more can we create the invariants and handle I/O. We’ll see. I will submit something this week (today or Wednesday) showing I/O, which isn’t in most verifications, can be verified. Just requires a different modelling style which should surprise nobody.

    2. 3

      This paper is starting to gain traction and the discussion needs to broaden out; mathematics suffers from the same problems as software development

      1. 1

        That On Proof and Progress paper was great! Appreciate you sharing it. There was quite a bit of overlap between what he said and another I was reading on fixing math education. Schools focus on equations and publishing too much when real math research is more about understanding and communicating with each other. That one indicates, though, that there’s significant, avoidable problems in traditional math on communicating as well.