Kevin Lacker

We're making a big change to the Acorn syntax: using square brackets for type parameters, instead of angle brackets.

Before:

inductive List<T> {
    nil
    cons(T, List<T>)
}

After:

inductive List[T] {
    nil
    cons(T, List[T])
}

Acorn 0.1 is out! It might not be obvious at first, but there's a big change in the guts of how the prover works. When a proof is successfully verified, the build directory now contains a "proof certificate" explaining step by step how the proof works.

Typeclasses in Acorn provide a powerful way to define common behaviors across different types. But what happens when you need to build upon existing typeclasses? Today, we're introducing typeclass extension.

Since launching the Acorn beta, we've heard consistent feedback from mathematicians that they need a powerful type system to represent their favorite area of mathematics.

Today, we're releasing two big improvements to Acorn's type system. The first is typeclasses.

There's a useful new feature in Acorn Prover 0.0.8: a build cache.

When you save changes to an Acorn project, the AI model automatically completes simple proofs with missing steps. Usually this works great, but this can make refactoring more difficult. In particular, if you make changes to a module like nat.ac that many other modules depend on, it can be slow to rebuild everything. If you want to remove a theorem that is used in many places, this can involve many slow rebuilds.

We've deployed a new version of the Acorn Prover, 0.0.5, with support for a commonly requested feature: generic types. For example, the standard library now has a Pair structure:

structure Pair[T, U] {
    first: T
    second: U
}

Good news, everybody!

With this blog post, I hereby demonstrate that the Acorn blog is now capable of handling posts.