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

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.

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

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.

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

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

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.

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?

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

Comments URL: https://news.ycombinator.com/item?id=30029388

Points: 3

# Comments: 0

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.

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

  bar = fmap (fmap foo) getNM

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?

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