HN Showcase
Back to browse
Pantagruel, an Accessible Specification Language

Pantagruel, an Accessible Specification Language

by crux·Feb 23, 2026·4 points·0 comments
Visit ProjectView on HN

AI Analysis

●●SolidBig BrainNiche GemZero to One

TLA+ or Alloy for people who aren't PhDs, but adoption depends entirely on community.

Strengths
  • •Radically simpler syntax than TLA+/Alloy with genuine type system and model checker—solves real pedagogical barrier.
  • •Domain-agnostic (poetry, games, business rules)—shows thinking beyond software specifications.
  • •Seven years of iteration with documented type theory suggests serious rigor, not a prototype.
Weaknesses
  • •No evidence of real-world adoption, users, or production specs—competitive advantage is theoretical.
  • •Model checker scope and performance limits unknown; unclear how it scales vs. industrial tools.
Target Audience

Software engineers, formal methods practitioners, systems designers, anyone wanting to formalize ambiguous requirements.

Similar To

TLA+ · Alloy · Coq

Post Description

Hi HN!

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.

Similar Projects