Seven years ago I posted the very first version of PANTAGRUEL (my phone has started autocorrecting to all-caps; I have no idea why but I like it), a “lightweight formal methods” language.

Since then it’s gone through many iterations. I want to post it here because in the recent months it’s acquired a consistent, well-formed and documented type system, and an actual model checker.

In other words, it’s now a language of the same kind as something like TLA+ or Alloy. It differs from those in being (hopefully) radically simpler. It’s designed to be approachable with far less learning and specialization, and it’s designed to be effective in specifying not just software, but any type of formal system, including poetry and games.

If you’ve ever been interested in “tools for thought” and ways to make your own descriptions of things more precise and rigorous, it might be worthwhile to you.