Gajurgensen

I didn't mean to imply that the US is more likely than elsewhere to responsibly steer AI via policy. But I do think it is easier if it can be done internally as opposed to via international dealmaking.

It is incredibly important to whether the US can maintain its AI lead. If foreign competition is closing the gap only by distillation, then the frontier labs can focus on preventing distillation and maintain their lead that way.

US dominance is also important for approaches to safety, especially political approaches. If the frontier models are all US-based, safety might be tackled via internal US policy. If other countries can independently train competitive models, international cooperation is required.

Edit: It is also important for the business model. Companies won't be able to justify tremendous training costs if competitors can replicate their product much more cheaply via distillation.

I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing very explicit proof objects directly, because it allows the obvious but tedious details to be elided. What you are left with are just the most important high-level steps that the automation couldn't infer (or which we just don't wish to delegate). Things like "induct according to this scheme after generalizing this variable" or "first prove this auxiliary lemma" or "apply this inverse function to both sides so that they cancel".

I'd also argue that automation is essential to practical proof engineering. It make the proofs less brittle to minor changes and therefore more maintainable.

Edit: a couple more thoughts. First, there is nothing stopping you from defining proof objects directly in Lean without tactics. That flexibility is quite nice -- you can automate as much or as little as you like. Of course, in practice, people almost always use tactics. Second, I use the ACL2 prover quite a bit, which is not tactic-based. Instead, you give high-level "hints" that steer the aggressively-automated prover. Funny enough, I have colleagues that look at Lean proofs and say "these proofs are so verbose, how does anyone understand them!".

I was referring to issues that arise around the need for heterogeneous equality.

As an example, consider the dependent vector type `Vec n`, which is an array of length `n`. An `append` function would have type `{n m: Nat} -> Vec n -> Vec m -> Vec (n + m)`. That is, it takes an array of length `n`, and array of length `m`, and produces an array of length `n + m`.

Now imagine that you want to show that `append` is associative. That is, for all `x: Vec n`, `y: Vec m`, and `z: Vec o`, you have `append (append x y) z = append x (append y z)`. We can't prove this because we can't even state the theorem; it is not well-typed. The left-hand side has type `Vec ((n + m) + o)`, while the right-hand side has type `Vec (n + (m + o))`. Those two length values are of course propositionally equal, but they are not definitionally equal in type theories like Lean or Rocq's. That is, the equality is not immediately apparent to the type checker, and so requires a proof. But even with a proof, the statement is ill-typed (because equality is "intentional", not "extensional"). So you have to use a heterogeneous equality operator which allows you to compare two values whose types are propositionally but not definitionally equal. This equality is generally more difficult to work with.

Obviously this whole problem goes away if we use a non-dependent array type, as opposed to something length-indexed like this `Vec` type. So unless there is some reason to use the indexed type (e.g., perhaps the compiler can emit more efficient code), I would just use the non-indexed types and prove separately anything I want to know about the length.

I think the question of "necessity" is interesting, because between establishing that something is necessary vs the best option, I'd say the former is easier. And by agreeing that dependent types are not necessary (at least for certain design goals) we give space to the folks creating new provers to experiment with alternatives, which I think that is a good thing. I have been extremely impressed during my limited interactions with Lean, but I'm also vaguely aware of enough pain points to be interested in what other provers can do without being based on curry-howard.

Anyway, for what its worth, I generally agree that static typing is preferable. It is just a little more complicated in the context of theorem provers (as opposed to general-purpose, non-verification programming languages) where, for provers not based on type theory, propositions and proof obligations can be used where we might otherwise use types. This can be nice (generally more flexible, e.g. opportunities for non-tagged sums, easy "subtyping"), but also can be a downside (sometimes significant work reproducing what you get "for free" from a type system).

Very interesting. My takeaway is that Dr. Paulson's answer to the question is that there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary.

I would have liked to read more about Lean's alleged performance issues, and the issues around intentional equality. For the latter, I understand one can run into the need for heterogeneous equality (https://lean-lang.org/doc/reference/latest/Basic-Proposition...) when types are propositionally equal, but not definitionally equal. It has been some time I worked seriously in a dependently-typed language, but I recall coming to the conclusion that dependent types are best used as little as possible, for exactly this reason. If something may be stated as a theorem after the fact instead of putting it in the type, that was my preference.

Certainly there is something strongly aesthetically appealing about dependent type theory. The unification of programs and proofs and the natural emergence of independent proof objects. I am open to the idea that overly-dogmatic insistence on a type-theoretic basis to a theorem prover could lead to pragmatic issues, but I'd need to see more examples to be convinced there is a better foundation.

Anyway, I agree with Dr. Paulson's point that dependent types aren't necessary to verify interesting systems. He talked more of pure mathematics, but I am more interested in software verification. I work heavily in ACL2 which, not only does it not have dependent types, it doesn't have static typing at all! It is, however, also a first order logic and the both of these facts can sometimes be frustrating. Various libraries have been introduced to simulate typing and higher-ordered reasoning.

Think of higher level specifications which do not imply any details of the implementation.

For instance, consider a sorting function. One could write a bubble sort and consider that a spec, but that is far too much detail, much of which you don't actually care about. A much better specification would be "the function takes a list 'l' and produces a sorted list which is also a permutation of 'l'." This is the sort of specification we want, but we have more work to fill in the implementation details.

This can get arbitrarily difficult if your specification logic is sufficiently expressive. Imagine the spec is something like "solve this unproven mathematical conjecture."

Program synthesis is of course very difficult in general, especially if you want it to be entirely automated. One option to make it more practical is to have the user drive synthesis from specification to implementation via something which looks like a sequence of tactics.

(I'll add a plug to some stuff we are working on at Kestrel: https://www.cs.utexas.edu/~moore/acl2/manuals/latest/index.h.... We've used the APT library to do stepwise refinements from specs ACL2 to C code. Each step is something like "make function tail recursive" or "switch to a new, isomorphic shape of the data").

By the way, Curry-Howard offers a compelling insight here: deriving programs from specifications (i.e. types+propositions) may be the same process as deriving proofs from propositions. So the two processes can in principle work the exact same way.

Very interesting work! I'm curious how you handle loops/recursion? I imagine the `M` monad seen in the examples has a special primitive for loops?

Theorem provers aren't just for mathematicians formalizing mathematics. Although, for that purpose, Lean seems to be very popular these days (perhaps followed by Coq?). Theorem provers are also used to formalize software and hardware systems. The people using theorem provers are diverse in their tasks and priorities.

Consider three provers/languages: Coq, ACL2, and Dafny.

Coq is a very expressive, dependently-typed, higher-order functional language, much in the spirit of Haskell or SML. It is very powerful for writing specifications due to this expressivity, and is therefore a compelling candidate for formalizing mathematics. It also has a very clean separation between proof search and proof checking, allowing for a smaller trusted kernel in the proof checker. However, due to the complexity of the language, writing proofs tends to be a largely manual task, or require domain-specific automation.

ACL2, on the other hand, is simpler in its language. It is a first order logic, built atop a total, untyped (at least logically) lisp. It does not produce proof artifacts like Coq, but proofs are much more automated, consisting of only a handful of hints instead of an entire tactic-tree.

Finally, Dafny is an imperative language, very much resembling popular and ubiquitous languages familiar to every programmer. Proofs are managed by adding inline annotations, specifying pre and postconditions, invariants, etc. This does not expose hardly any of the proof internals, and may be difficult for large proofs, but is a relatively friendly interface for the working software engineer.

Coq is constructive be default, but you can add the axiom of choice and the law of the excluded middle to make it classical (other common axioms are functional extensionality, propositional extensionality, and proof irrelevance).

Perhaps you are recalling Godel's incompleteness theorem, which says that for any finite formal system (like Coq) there exists a true theorem it is unable to prove?

ACL2 has a documentation page for the theorems from this list proved: https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/in...

A couple of theorems have actually been proved but not yet reported/counted.

That's an awfully long-winded and confusing way to say you think "Boolean blindness" is too nitpicky. Personally, it seems like a pretty valid idea to keep in mind, especially as developers transition from a conventional imperative language to Haskell. Making frequent boolean checks is pretty normal in that space, and pattern matching is less common, which might lead new Haskell programmers to write unidiomatic code.

The encoding of natural numbers in lambda calculus can be mysterious at first glance. I'm surprised the author didn't spend more time on it. No need to be so hostile about it though.

Essentially, we represent numbers as functions that will call a function a number of times on a base value. So for `zero = λs. λz. z`, we can see if we gave it a function `s`, and a value `z`, it would apply `s` zero times to `z`. For `one = λs. λz. s z`, clearly `s` is applied once to `z`. I think you can see the rest of the pattern. Its really as simple as that.

We can then define the successor function as `suc = λn. λs. λz. s (n s z)` (I'm not sure why the author doesn't write this out. Instead he confuses the successor function with the `s` argument). We can see `suc` behaves as expected with examples. `suc one = (λn. λs. λz. s (n s z)) one = λs. λz. s (one s z) = λs. λz. s ((λs. λz. s z) s z) = λs. λz. s (s z) = two`. All we need is our definition of `zero` and `suc`, and we can define any natural number.

Now go back and look at the definition of `plus` and it should make a lot more sense.

Let's say getting those n and m values has a nasty type like `getNM :: IO (Maybe (Int, Int))`. All you need to do is map twice when using the original function.

  foo (n, m) = take n . filter p . drop m

  bar = fmap (fmap foo) getNM

It's a little awkward, but no major refactor. A small price to pay for the nice types we get. I'd argue that if other languages make dealing with IO and optional values easier, its because they don't bother restricting IO (not necessarily criticizing that), or they don't bother checking completeness over optionals (i.e. a stray `null` can show up anywhere and derail the program, which I do think is a bad thing). Overall, Haskell provides many powerful tools for composing complex types, such as the functor/applicative/monad classes.

I highly recommend people interested in Coq start with Pierce's Logical Foundations. It is by far the most accessible introduction to Coq I've found. I'm working through Chlipala's books next. CPDT is a great deep-dive into more advanced use cases of Coq as well as its theoretical underpinnings. I'll be taking a class this semester based on FRAP, my understanding is it hits those formal methods and language topics without specifically emphasizing Coq, except for the exercises.

As an aside, since Coq is the only theorem proving language I know well, I am curious what the pros/cons are as compared to Isabelle/HOL, F*, Lean, etc. Coq has been around for a while, but I keep seeing new theorem provers pop up. What are the alleged weaknesses of Coq that other languages are trying to fix?

I understand that the pervasive cynisicm can be exausting, but in the case of computer security, it really is warranted.

It would be nice if there was a standard type alias for Either which explicitly labeled good/bad values.

That being said, I don't think it takes that much energy to remember that the right is the good value. If you are comfortable with monads, just remember that monads must be parameterized over a single type, and for Either that will be the right type (because we must partially apply the type constructor with the left type to get it down to the correct form).

This is great! It's not going to replace proof general + (evil mode) emacs for me, but this would be a great way to introduce people to Coq without worrying about installation.

> Rust achieves impressive numbers with the most obvious approach. This is super cool. I feel that this behavior should be the goal for any language offering these kinds of higher order functions as part of the language or core library.

Certainly it should be a goal, but I don't think it should be the goal. Higher levels of abstraction aren't typically motivated by performance. The priority is ease of expression and reasoning about code. Of course both are desirable, but when the two are in conflict and a trade off is necessary, designers will lean toward expressive abstractions, not performant abstractions. After all, performance is already available without the abstractions.

But I do agree it is super cool how Rust finds a sweet spot between performance and expressibility. It is one of my favorite languages for that reason. I just don't think it should be a universal goal.

This is pretty nitpicky, but I really dislike the postfix syntax for type constructor application.

Why wouldn't it be a good solution to write something like Box, but with a new function that returns `Option<Box<T>>`? I'm not sure what Rust is lacking here.

Learning about Church and Scott encoding was much more interesting than I thought it would be. I was expecting it to be tedious and banal, but I came out of it feeling like I had some sort of revelation. Imagining naturals, lists, trees, etc. as function application was mind-bending at first, but it eventually clicks into place. Lambda calculus is so incredible in its combination of simple semantics, expressiveness, and abstraction/compositionality.

To go a step further, think about how you would implement a predecessor function on the Church encoding of the naturals. It is much more complicated than one might expect, and perfectly motivates the introduction of Scott encodings and the fixed-point function.

If I recall correctly, most CakeML code is actually written in HOL4 and then translated down to CakeML, and compiled to machine code from there. Unfortunately there isn't very much in the way of documentation or examples for writing concrete CakeML, as the developers seem to use it more as an intermediate representation.

Edit: The page describes two frontends. The first is a "proof-producing synthesis" of a CakeML AST from "ML-like functions in HOL". This is what I believe is the more typical use case of CakeML. The second frontend is a more traditional frontend which parse concrete CakeML syntax.