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

Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so roughly a kernel resource). Over that, you build a huge amount of (userspace) tooling that doesn't have to be absolutely trusted since its job is just to talk into the kernel and get theorems.

A kernel bug manifests as the kernel deciding that something is a theorem which shouldn't be. The worst case is when it decides that False is a theorem, from which it immediately follows that absolutely everything is a theorem.

The HOL Light kernel (mentioned in the article) is about 500 lines from one file (https://github.com/jrh13/hol-light/blob/master/fusion.ml), and is a very straightforward implementation of a simple type theory (https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations). I'm not so familiar with Lean, but it would appear its kernel is spread over this C++ directory: https://github.com/leanprover/lean4/tree/master/src/kernel.

As mentioned in the article, HOL Light gets away with a lot because it only cares about delivering theorems. Other systems want to retain the proofs as artifacts (sometimes called certificates), and once you do that, you need to make sure these artifacts aren't stupidly huge or otherwise useless. Provers such as Rocq (and I assume Lean) additionally want their proof objects to contain decent executable algorithms backing the proof.

HOL Light also does pretty much no evaluation. The most it understands of evaluation is that (λx. f) x = f. If you want to evaluate anything more complex than this, you build that in "userspace" and you do all the equational reasoning manually via the kernel.

Lean and Rocq kernels do full evaluation of recursive functions, so they have to come installed with an API for building those recursive functions and internal checking to make sure those functions are terminating. The article's author is asking whether you could redo something like Lean and Rocq where the recursive function API was much simpler. I've wondered for a while whether you could also have the evaluator as basic as HOL Light's, and do the rest in userspace. I think there were theorem provers like this that went out of fashion decades ago.

It used to be a much more exciting space before Lean somehow got everyone's attention. The author is the co-creator of Isabelle/HOL, and is still not sure why there is so much more excitement for Lean than for simple type theory.

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.

> The pipe operator works similarly, though it's a combination of fork and dup'ing

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

Yes, as I said: systems such as Russell's encoded "1", "2" and "+" in such a way that the theorem "1 + 1 = 2" is non-trivial to prove. This doesn't say anything about the difficulty of proving that 1 + 1 = 2, but merely the difficulty of proving it in a particular logical encoding. Poincare ridiculed the Principia on this point almost immediately.

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.

> Anyone who says AI is useless never had to do the old method of cobbling together git and ffmpeg commands from StackOverflow answers.

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.

There isn't a serious proof that 1+1=2, because it's near enough axiomatic. In the last 150 years or so, we've been trying to find very general logical systems in which we can encode "1", "2" and "+" and for which 1+1=2 is a theorem, and the derivations are sometimes non-trivial, but they are ultimately mere sanity checks that the logical system can capture basic arithmetic.

There's no point as such. They are a natural (non-leaky) generalisation of a recurring pattern in mathematics and software over which you can build some general theory and, in the case of programming languages such as Haskell, a general purpose library.

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.

Playing "This thing all things devours" is one of the most profound gaming experiences I have had, and I happened to use Malyon. Why wouldn't I use the best text editor to play an inform game?

"Tuttle? His name's Buttle. There must be some mistake."

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

I love the idea of hanging by a thread, of complete existential and cosmic precarity. To again quote the opening of Call of Cthulhu, science will reveal "our frightful position [in reality]". I like the fact that, for Lovecraft, the answer to such terrifying revelations is mostly to draw the curtains and ideally brick up the window and insist "nothing to see here." The opening quote offers that as one solution, but it's recurrent in his stories. It's what the protagonists end up doing in the Dunwich horror mentioned in the blogpost.

I'm the opposite. One of the things I love about Lovecraft is how oblique the mythology is in his writings. I don't know much about Azathoth, save that he's somehow "Lord of all Things", while being a "Blind Idiot God." That seeming contradiction is tantalising and the last thing I want is to see it fleshed out.

It's fear of the unknown, after all, not fear of the things that have detailed wiki pages.

The article mentions ST Joshi a few times, who I think deserves credit not just as the foremost scholar of Lovecraft, but possibly for bringing attention to Lovecraft in the 60s and 70s. I thoroughly enjoyed his "Decline of the West", which pores over Lovecraft's correspondences trying to get a broad handle on his philosophy and aesthetics. He strikes me as a pretty complicated individual, with his early bigotry and his later slightly less malignant cultural chauvinism always being at odds with his cosmicism. And I think his nostalgic, escapist fantasy might generally have been at odds with his uncompromisingly scientific realism, perhaps contributing to his somewhat bitter and bleak view of the sciences (each straining in their own direction).

(I once owned one of those cute green Cthulhu plushies)

You use them all the time in Haskell and OCaml. Cache locality isn't such an issue. You're not mallocing linked list nodes. You allocate by a pointer bump of the minor heap, and if the GC copies your list into the major heap, it's going to copy the list elements together.

You also use recursion all the time, and no, recursion is not generally straightforwardly optimised into iteration unless you're doing trivial tail recursion.

When I started using CL 20 years ago, libraries were stored on cliki and any malicious user could put malware there. Any source you asdf-installed was generally GPG signed and the installer automatically checked signatures against your personal trust-chain.

Learning CL back then was my first introduction to GPG (and Emacs, and Linux)

I have been playing again with CL recently and am doing some trivial web-scraping of an old internet forum. I don't use a REPL directly, but just have a bunch of code snippets in a lisp file that I tell my editor to evaluate (similar to Jupyter?). I haven't bothered doing any exception (condition) handling, and so this morning I found this in a new window:

   Condition USOCKET:TIMEOUT-ERROR was signalled.
      [Condition of type USOCKET:TIMEOUT-ERROR]

   Restarts:
    0: [RETRY-REQUEST] Retry the same request.
    1: [RETRY-INSECURE] Retry the same request without checking for SSL certificate validity.
    2: [RETRY] Retry SLIME interactive evaluation request.
    3: [*ABORT] Return to SLIME's top level.
    4: [ABORT] abort thread (#<THREAD tid=17291 "worker" RUNNING {1001088003}>)

plus the backtrace. This is in a loop that's already crawled a load of webpages and has some accumulated some state. I don't want a full redo (2), so I just press 0. The request succeeds this time and it continues as if nothing happened.

At various times, I have run a Tor relay node on a spare VPS. I think I stopped in the end because my available bandwidth was pretty below par, and I suspected I wasn't helping the network very much.

Just my understanding of the manpage and TCP forwarding (-L): an SSH connection will be established to the jump host, which then establishes a connection on port 22 to the destination. The local machine now has a forwarded connection to the destination and uses that to establish a second SSH connection between them.

Between local and jump host, there will be two layers of encryption. The jump host decrypts the outer layer, and the two ends the inner layer.

Specifically, Awk is a good solution to a problem that should never have existed in the first place. Why am I having to write these bespoke parsers for the random mess of output formats that you get from the UNIX command line?

Well, the fact is that I have to write such parsers. That's very sad, but has no chance of being fixed. So it's good to know Awk.

I think Erik Naggum had this exact criticism of Perl.