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

I wonder if AI systems like ChatGPT will be helpful in this area. Something that’s able to track all requirements of a system and understands the code enough to validate it against the requirements.

I've always thought theorem proving to be about proving equality of the function and the result.

Lean to me is not only obscure but unapproachable by someone from a non-mathematical background.

Take this snippet for instance

      theorem nat.add_comm : ∀ (n m : ℕ), n + m = m + n :=
      λ (n m : ℕ),
      nat.brec_on m
         (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) m) (n : ℕ),
            nat.cases_on m
               (λ (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) 0),
                  id_rhs (n + 0 = 0 + n) (eq.symm (nat.zero_add n)))
               (λ (m : ℕ) (_F : nat.below (λ (m : ℕ), ∀ (n : ℕ), n + m = m + n) (nat.succ m)),
                  id_rhs (n + (m + 1) = nat.succ m + n) (eq.symm (nat.succ_add m n) ▸ congr_arg nat.succ (_F.fst.fst n)))
               _F)
         n

If we want to democratise formal methods and theorem proving, we should lean towards natural language expressions of proof and not mathematical expressions and greek characters.

This is the path that languages such as Idris https://www.idris-lang.org/ have taken

I like there is us who like formal methods and guarantees of correctness for our code.

And then there are the others who now generate approximately code with large language models that mostly runs.

They are winning.

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.