[ANN] Packages for making proof assistants

We are excited to announce the first release of asai 浅い on OPAM, along with new versions of algaeff and yuujinchou 友人帳. We also released bwd and mugen 無限 on OPAM earlier but didn’t make an announcement.

All these packages are part of our research project to dissect a typical proof assistant into composable components so that everyone can easily build a high-quality, usable prototype out of their type checker. It turns out that many components are useful for writing compilers, too. Here are our packages: (:white_check_mark: means it’s on OPAM.)

together with these more general-purpose packages:

  • :white_check_mark: algaeff for well-known composable effects-based gadgets (e.g., state, reader, etc.)
  • :white_check_mark: bwd for backward lists

We have a prototype system showing how these packages may be used together. Many packages have been used in our proof assistant cooltt, @jonsterling’s :white_check_mark: forester tool and Topos Institute’s polytt. We invite you to try out our packages the next time you want to build a proof assistant or compiler!