What I've Learned About Formal Methods in Half a Year

Sorry to hear you had issues with my comment system. Comments are invisible until I manually approve them, but I'm not seeing anything new in the database right now. Did you get any sort of error code? The system should let you know if e.g., the answer to the captcha was wrong.

I do mention SPARK at the end of the article. I'm not familiar with Frama-C so I'll check that and your blog posts out. Thanks for sharing!

I think the interesting part isn't in a single component's edge cases at all, but in how complex webs of many, many things interact.

I've yet to see a hard debugging problem that didn't boil down to something like, in the best of possible worlds:

"component A expected something to meet promise FOO when it calls component B, because that's obvious, right?" combined with

"component B just passes requests and routes results, dude, component C is messed up" combined with

"component C never promised that behavior and if you look at our spec it even says so!"

That's an example of your "does not match what was expected" case.

I think most of formal methods is an academic waste of time. Whether they take a more formal or a more practical approach, I see high value in contract tests and data flow analysis because they're more likely to catch the bugs that cross Conway's code/org boundaries.

You don't need to prove everything against a complete spec, you can prove that things have particular properties you care about, from higher level behaviors like user data can only be accessed by the user down to there are no out of bounds array accesses.

You could prove some complex data-structure to be a correct implementation of some logical data-structure and then prove that your service won't deadlock.

There are a ton of interesting, impactful properties to prove that aren't "create a complete specification and prove the implementation refines it", and even that usage I think is more impactful for removing bugs and vulnerabilities than you're giving it credit for - even something as simple as sorting, Java had a bug in their Timsort implementation for a decade which was discovered when trying to verify it with formal methods: http://envisage-project.eu/wp-content/uploads/2015/02/sortin... ). Note too that if you compiled the simplest/easiest-to-understand spec for something like sorting you'd get something like bubble sort, not Timsort, though you are much more likely to want the latter.

> I think I would just be easier to hit compile on that spec

I have a hard time not being similarly skeptical about formal methods. They promise the ultimate holy grail of software development - release software with zero defects - but demand what appears to be years of study before you actually see results. On the one hand, there's lots of examples of techniques and tactics that promise amazing results if you "put in the work", even outside of software (like fitness and music) - but in over 30 years of software development practice, I've never met anybody who was applying formal methods at all, much less to achieve defect-free software. If it could deliver what it promised even with a "mere" five years of dedicated study, I'd expect it to be more widespread by now.

One advantage of formal methods is in determining "what was expected" (including all the goofy edge cases) without having to burrow into the details of code.

Take a look at Alloy (http://alloytools.org/) and TLA+ (https://lamport.azurewebsites.net/tla/tla.html) for example. (Or even the ancient Z ("Zed") notation (https://www.cs.cmu.edu/~15819/zedbook.pdf)).

It’s a repeat of search & hope/trust (Google) vs define and query (semantic web) and yes they are winning and will win. Fine tuning your scope for extreme accuracy might be less efficient a strategy than fine tuning your loader for extreme speed

Ship early, ship often. First to ship wins. Flood the zone.

Often phrased as "worse is better."

Like, hypothetically, imagine you spent two whole weeks designing and implementing a new programming language, which was guaranteed to be installed on millions of computers overnight. Any language which took three weeks to finish, like wasting a week testing, would be DOA.

Like how the (brood parasite) cuckoo chick hatches early and then murders all the other chicks.

But when the robot uprising comes our killbots will be unstoppable terminators and their killbots will explode the first time they encounter a set of stairs.

When the latest incarnation of ChatGPT was out, I had the same thought. However, I then became convinced there might be some synergy between both.

Imagine a programming system where you can specify little components using Hoare or Separation Logic, i.e. pre/postconditions. An engineer could spend his effort specifying little components, but code and proof generation can be handled by GPT. Actually, many tasks can be offloaded to a SAT/SMT solver. Lots of verification and synthesis efforts already do the last bit, offloading to SAT/SMT solver.

This would be a win-win. Formal methods would become cheaper to use, and software would become built using rigorous engineering.

Do you have more to share? I use Alloy at work and research and would love to learn about how Apple uses FM.

ChatGPT is basically the opposite of formal verification...

It itself is not verified, and its results are so inaccurate that you need to verify them anyway.

Most definitely. I've been playing with using ChatGPT to generate proof texts in Isabelle/HOL, since it lets me verify the correctness of the output before code generation.

I've had the same thought. Formally proven code can give powerful security assurances (cf. Project Everest[1]), but it's also very, very labor-intensive. I've heard rules of thumb like, "100x as much time to prove the software correct as to write it in the first place."

If LLM systems are going to give us a virtual army of programmers, I think formally proving more systems software (device drivers, browser engines, etc.) would be a great use of their time.

[1]: https://www.microsoft.com/en-us/research/blog/project-everes...

Yeah, I'm cautiously excited about how AI and FM might work together. I don't think LLM's can ever be trusted to verify programs itself, but anything which can reduce the annotation overhead for programmers is a super useful thing!

There is ongoing work trying to get that marriage to work

I don't think you have any chance of approaching formal methods if the notation is a stumbling block.

The difficulty and verbosity of formal proofs is huge even with the very concise mathematical notation. And learning the notation itself is a very small stumbling block compared to learning the actual theorems and logic that you need to use.

So while I am not a fan of mathematical notation for general programming (which is often quite un-mathematical in fact) formal proofs are a place where this notation absolutely shines. I can't even imagine how much uglier the proof above would become if you had to replace `∀ (n : ℕ)` with something like `for any natural number n`.

I sympathize with your view, I genuinely do, but to write out formal methods using natural language expressions results in quite a few problems. For one, it results in incredibly long proofs, like this simple proof written out in natural language would take up pages.

Second, it makes it harder to identify patterns. Writing things out in a formalism lets you identify syntactic patterns and employ techniques like factoring, cancelling, seeing symmetries and other purely syntactic properties. When you write things out in natural language you lose the ability to see these things clearly. Being able to see purely formal syntactic properties helps reinforce your confidence in a proof or can help you identify potential flaws in it. It's like with programming styles and conventions, one thing I tell developers is an important reason for choosing one style over another is if it makes wrong code look wrong visually.

Third, and this is just a personal matter... it results in a type of culture of writing that I find is often pretentious and full of unnecessary baggage. When I read an academic paper I cringe at how bad most writing is and try my best to skip to the formal part of the paper.

> if we

Who is this we? The people who understand mashed with the ignorant who put in no work?

> to democratise

So that those in the know can be further diluted with dabblers who contribute nothing and complain about their ignorance?

That snippet is the result of printing out the internal structure of the proof, not how the proof was actually written. You'll notice that what a human actually wrote and would normally read is the code block mentioned directly above in TFA, which is much more sensible:

  lemma nat.add_comm : ∀ n m : ℕ, n + m = m + n
  | n 0     := eq.symm (nat.zero_add n)
  | n (m+1) :=
    suffices succ (n + m) = succ (m + n), from
      eq.symm (succ_add m n) ▸ this,
    congr_arg succ (add_comm n m)

Also, this example proof is explicitly about math (the commutativity of addition on natural numbers), so it's appropriate and not surprising that it uses mathematical notation.

Something else important to note: this proof of commutativity of addition on natural numbers is definitely _not_ how you normally write these proofs in Lean.

Here is a closer approximation to how someone would actually write the proof in Lean:

  lemma add_comm (a b : ℕ) : a + b = b + a :=
  begin
    induction a with a IH,
    rw (add_zero b),
    rw (zero_add b),
    trivial,
    rw (add_succ b a),
    rw (succ_add a b),
    rw IH,
    trivial
  end

One thing which perhaps is not captured well in the article, is that rather unlike when reading/writing source code, where stepping through lines of code is a relatively uncommon task only done debugging. For interactive theorem provers it is a given. He discusses the bottom up & top-down approach to the solving goals with tactics & otherwise, but typically in both cases you will be stepping through expressions to get a better understanding. They generally aren't written to be read from just the source text alone.

Brute force string search:

    /*@
      // There is a partial match of the needle at location loc in the
      // haystack, of length len.
      predicate partial_match_at(char *needle, char *haystack, int loc, int len) =
        \forall int i; 0 <= i < len ==> needle[i] == haystack[loc + i];
     */

    /*@
      // There is a complete match of the needle at location loc in the
      // haystack.
      predicate match_at(char *needle, int n, char *haystack, int h, int loc) =
        \valid(needle + (0 .. n-1)) && 0 <= n < INT_MAX &&
        \valid(haystack + (0 .. h-1)) && 0 <= h < INT_MAX &&
        n <= h && loc <= h - n &&
        partial_match_at(needle, haystack, loc, n);
     */

    /*@
     requires \valid(needle + (0 .. n-1)) && 0 <= n < INT_MAX;
     requires \valid(haystack + (0 .. h-1)) && 0 <= h < INT_MAX;
     requires n <= h;
     assigns \nothing;
     ensures -1 <= \result <= (h-n);
     behavior success:
        ensures \result >= 0 ==> match_at(needle, n, haystack, h, \result);
     behavior failure:
        ensures \result == -1 ==>
          \forall int i; 0 <= i < h ==>
            !match_at(needle, n, haystack, h, i);
     */
    int
    brute_force (char *needle, int n, char *haystack, int h)
    {
      int i, j;
    
      /*@
        loop assigns i, j;
        loop invariant 0 <= i <= (h-n) + 1;
        loop invariant \forall int k; 0 <= k < i ==>
          !match_at(needle, n, haystack, h, k);
       */
      for (i = 0; i <= h - n; ++i) {
        /*@
          loop assigns j;
          loop invariant 0 <= j <= n;
          loop invariant partial_match_at(needle, haystack, i, j);
        */
        for (j = 0; j < n && needle[j] == haystack[j + i]; ++j);
        if (j >= n) {
          return i;
        }
      }
      return -1;
    }

> Lean to me is not only obscure but unapproachable by someone from a non-mathematical background. ... If we want to democratise formal methods and theorem proving ...

For whom is that a goal? Are there really that many individuals at the intersection of "I need to use a theorem prover" and "I don't have formal mathematical training"?