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)

  X = xz + xw + yz + yw

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.

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.

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.

> 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

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

"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, ..."

   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)

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, ....

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)

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

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).

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

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.

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.

Any time the shell executes a program it forks, not just for redirections. Redirections will use dup before exec on the child process. Piping will be two forks and obviously the `pipe` syscall, with one process having its stdout dup'd to the input end of the pipe, and the other process having its stdin dup'd to the output end.

Honestly, I find the BASH manual to be excellently written, and it's probably available on your system even without an internet connection. I'd always go there than rely on stack overflow or an LLM.

https://www.gnu.org/software/bash/manual/bash.html#Redirecti...

And had Russell failed to prove that 1 + 1 = 2 in his system, it would not have cast one jot of doubt on the fact that 1 + 1 = 2. It would only have pointed to the inadequacy of the Principia.

It's useful for that yes, but I'd rather just live in a world where we didn't have such disasters of CLI that are git and ffmpeg.

LLMs are very useful for generating the obscure boilerplate needed because the underlying design is horrible. Relying on it means acquiescing to those terrible designs rather than figuring out redesigns that don't need the LLMs. For comparison, IntelliJ is very good at automating all the boilerplate generation that Java imposes on me, but I'd rather we didn't have boilerplate languages like Java, and I'd rather that IntelliJ's boilerplate generation didn't exist.

I fear in many cases that if an LLM is solving your problem, you are solving the wrong problem.

Haskell is one of the few languages that lets you write those general purpose libraries. In other languages, there's really no point talking about monads.

"Mistake? Ha! We don't make mistakes."

Proceeds to drop ceiling plug through ceiling.

"That's bloody typical. They've gone back to metric without telling us."