momentoftop

In HOL Light? Just so you can run the proof objects through another prover like Isabelle. Wasn't that your original ambition?

As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contain executable code, often of the very programs they were verifying, and so treat their proof assistants like programming languages with verifiers attached. So you get complex recursion and inductive definitions baked into the kernel. Whether this is a good idea or not is obviously pretty disputed among us, though I'm mostly with you and Larry :)

Converting natural language steps to a formal language isn't too challenging. But basically none of those steps will follow directly from the previous steps by any primitive deduction rule of any formal system. From the perspective of formal logic, there are massive gaps in the reasoning, and these need to be filled to pass the verifier. And they are absolutely massive, so massive that it would be completely intractable to fill them in manually.

That's where most of the tech in a theorem prover exists: its tooling to automatically fill in the gaps so your proof can pass the verifier. The tools and automation here are genuinely great, but you still end up having to write way more steps and inferences than you'd see in any maths textbook, and the details are far more fiddly because the formal verification is not very forgiving.

As an illustration, consider how you get from:

  X = (x + y)(z + w)

to

  X = xz + xw + yz + yw

The second equation doesn't follow directly from the first in any logical system. Instead, it follows by the distributive law, commutativity and associativity of addition, commutativity of multiplication, symmetry and transitivity of equality, and you'll need to have some means to specialise these universal statements and reason about term substitution.

A modern prover will do simple algebra like this for you, but the tooling had to be built to do it. In other domains, the tooling just dies trying to connect what an average working mathematician or even a mathematics undergraduate would consider obvious, and you're stuck either having to elaborate massive tedium, manually guiding the automation, or having to write new bespoke tooling to fill the gaps.

Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the details by hand. In 1956, Newell came up with the Logic Theorist which was able to prove a decent chunk of the Principia automatically. When Newell informed him, Russell conceded that his manual efforts had turned out to be wasted effort.

I used HOL Light about 15 years ago. The vast majority of the proof details are done by a machine, generally split between term rewriting and then offloads to a generic automated prover for first-order logic. Your job then is formalising the theorem statements and orchestrating the automation, and the latter still takes an enormous amount of labour.

Around this time, we were getting excited about recommender systems for lemma selection. The idea was that you turn every theorem into a bunch of features and train a recommender system against the lemma needed to prove it. Then when you face a new problem, you use its features to recommend which lemmas are likely to be needed. You then throw those lemmas and your conjecture at a bunch of industrial strength automated provers, get the provers to come back with a minimal set of necessary lemmas, and then use your verified automated prover to do the real proof with a tractable set of inputs. It first got implemented in Isabelle/HOL as Sledgehammer, and was a massive improvement to tooling.

Now LLMs are here and the game looks completely different. I went back over some verification I spent a week on about 5 years ago, in a pretty obscure formal verifier called HOL Light, on a problem of my own making. I'd seen how terrible ChatGPT was at propositional logic a few years back, so this is the sort of thing I'd had in my back-pocket as an "impossible benchmark" for LLMs. So as a half-joke, I gave Claude the main theorem I wanted proving, hoping to watch it embarrass itself.

In a minute or two, it has come up with the same proof strategy I had used, proving four lemmas to get to the main theorem. This was impressive, but that's not the laborious part, and I was pretty confident it would die trying to prove just the first lemma. It has its four lemmas enumerated and goes to thinking, while I go off for a cup of tea.

I come back five minutes later and it has scratched off the first goal. I'm pretty shaken, and go off again trying to process that. Come back, the second goal has gone. And then the third. And then the fourth. And then, after just fifteen minutes, it's pulled off a week of my work, done it more efficiently, and near enough one-shotted each proof. That took me a while to process. I realised that if I had this 15 years ago, it would have done 95% of my PhD, which is to say that 15 years ago, I would have done a 20x more ambitious thesis.

I contacted my old supervisor, who said the theorem proving community are all on top of this, including the creator of HOL Light, now at AWS. HOL Light, incidentally, was used on what I still believe is the most ambitious mathematical theorem proving project to date, the verification of the Kepler Conjecture. The lead on that project recruited a team to get the proof through over about 5 years. Today, I wouldn't be surprised if he could have solo'd it in 6 months. The same goes for another extremely ambitious project, the verification of the seL4 microkernel. And for another open problem, I know there are people seriously wanting to get a verification of Fermat's Last Theorem, which sounded delusional 15 years ago, but sounds pretty plausible now.

Exactly where this goes, I am not sure. I suspect we can now start on verification projects that would have been insane to contemplate. But a few things concern me. One is that Lean seems to have all the mind-share. Maybe it deserves it, but there are very major and mature theorem proving technologies such as Coq (now Rocq), Isabelle, HOL Light, ACL2 and Mizar that I believe still win in terms of having the largest verification libraries and the biggest verified projects. These should not be forgotten about, since they will also probably have the most training data, having been going for many decades now.

The second is that verifying our crappy human specifications probably isn't going to fly. As the creator of HOL Light says, representation (how you formalise your problem domain) is still where it all matters, and the LLMs aren't very good at this. And neither are the writers of our current specs. Verifying that a piece of software meets the HTTP spec will be considered an achievement, but it's the wrong goal.

We'll need specifications that are modular and composable, that mesh together so that each piece is sanity checking the others. This is how we build mathematics, and it's how we'd need to build software. Specs need to be short and comprehensible, so that a human can verify them. If your spec is as long and complex as the implementation, it's worthless.

But I believe it is possible to design software from the ground up where the motivation is specification engineering rather than code engineering, and thereby the specifications become the only human-facing understandable part of software. The implementation is just some artifact that an LLM generates that nobody looks at unless they are curious. And I think LLMS today mean that "build the world over again" isn't as mad a thought as it used to be.

Those manuals were fantastic. I was still coding on our Beeb in the early 90s and I wanted the assembly manual. My dad ordered it from Acorn but it never arrived. Ended up going to the small claims court to get our money back.

In the late 90s, I wanted to learn x86 assembly and sent an email to Intel asking for their reference manuals. They sent four huge volumes to me for free. I've no idea whether that was a mistake, but I was very grateful.

I still can't believe any of us were able to write programs just from reading books, and I'm not sure to what extent that's even possible today. Even online documentation now seems really crappy compared to those old manuals.

I understood that MLton was mostly about performance. It does whole program optimisation and is prepared (or does?) monomorphise just about everything, and applies all of your functors at compile time, so that you've got something more like C++ templates but well-typed.

> SML/NJ's heap2exec was a bit clunky compared to the others.

Unlike the others, SML/NJ implements call/cc, so it's going to need to do something funkier.

   SMLofNJ.Cont.callcc

   > val it = fn : ('a ?.Cont.cont -> 'a) -> 'a

Isabelle is still a very active LCF proof assistant, and it's still written in Poly/ML. It's pretty aggressively concurrent under the bonnet, and leverages Poly/ML well for that. There's still HOL4, which predates Isabelle and is still going, and it also recommends using Poly/ML.

I mostly worked with HOL Light which started as a CAML project and now runs on OCaml.

I also loved:

"It looks like they're doing something purposeful and coordinated, something vast --- a timing channel attack on the virtual machine that's running the universe, ..."

Most of them have simple types and are easy to define in ML or Haskell.

   I : a -> a
   I x = x

   K : a -> b -> a
   K x y = x

   W : (a -> a -> b) -> a -> b
   W f x = f x x

   C : (a -> b -> c) -> b -> a -> c
   C f x y = f y x

   B : (a -> b) -> (c -> a) -> c -> b
   B f g x = f (g x)

   Q : (a -> b) -> (b -> c) -> a -> c
   Q f g x = g (f x)

There are, however, combinators that do self-application (crucially used in the definition of the Y combinator) and these do not have simple types.

Combinators were an attempt to do logic (and computation falls out) without having to mess around with variables and variable substitution, which is annoying and inelegant because you have to worry about syntax issues like variable capture. Combinators were an attempt to do logic with a much simpler and cleaner syntax.

So combinator logic starts with a really simple language, based on a small alphabet of primitive combinators. You can see a bunch listed on the webpage:

   I, K, W, C, B, Q, ....

These are the primitive bits of syntax. The only other feature in the language is the ability to apply one combinator to another combinator. You write an application of a combinator "x" to another combinator "y" as "x y", and for convenience, you treat these applications as left associative, so "x y z" means "(x y) z": that is, first apply y to x, and then apply z to the resulting combinator.

Two typical combinators are K and S, with which you can form more complex combinators like

   K K
   S K
   K K K
   K (K K)
   K (S K)

...

Combinators generally come with simplification rules, and the ones for K and S are:

   K x y = x
   S f g x = f x (g x)

With these, we can start doing interesting reductions like:

   S K K x = K x (K x) = x

Now the weird fact: we're suddenly Turing Complete. It turns out that every possible computation is expressible just by building a big combinator out of K and S and applying those two simplification rules. No other machinery is needed.

K and S are not the only combinators with this property, and others form an adequate Turing Complete basis.

If you've heard of the Curry-Howard correspondence (Curry was responsible for combinatory logic), then combinators provide probably the simplest example of it, since if you give combinators types, you realise you are working with what's called a "Hilbert style" deduction system for propositional logic, which is the simplest sort of formal logical system. Indeed:

   1. Hilbert's first two axioms for his version of the calculus are exactly the types for K and S above
   2. K and S are invocations of these axioms
   3. Application is modus ponens
   4. The combinator S K K above corresponds to the proof that p → p.
   5. The simplification of S K K x is proof normalisation (if you ever see the proof S K K x for some proof x, you should simplify it to just the proof x).

Or better yet, the y combinator is this: W S (Q (S I I))

The whole point is that we don't need no stinking variables.

> It's extremely rare that you need to (printf "%d %d" foo)

I write stuff like `map (printf "%d %d" m) ns` all the time. I daresay I even do the map as a partial application, so double currying.

Ah, thanks, didn't realise they put the whole manual into the manpage. For other tools (e.g. make), the info manual is complete but the manpage is just a summary.

Try "info bash" on your system. It's the same manual.

In Emacs, when I hit C-h i I get a menu of all my info manuals and I first read the bash one there.