Pantagruel: An Extremely Lightweight Specification Language

Specification = [String].

Pantagruel is a language for writing system specifications.

pantagruel thoughts: [Thought] ⇒ Specification.

It’s a computer language, but not as you might think of it.

The effects of evaluating a specification are nil—Pantagruel has no execution semantics.

eval spec = null.

eval spec: Specification.
check spec: Specification ⇒ Bool.

However, Pantagruel specifications can be checked to ensure that certain conditions have been met.

For instance, that you’ve defined all your terms by the end of your document.

(∀ s <: invoked-symbols spec ⇒
 first-invoked-in-head? s spec → bound-as-of? s (first-appearance s spec)
 first-invoked-in-body? s spec → bound-as-of? s (next-chapter (first-appearance s spec))) → check spec.

(Head, Body) = [String].
Chapter = (Head, Body).
Specification = [Chapter].

This allows a structured form of description where terms can be explained in gradually greater detail.

first-invoked-in-head? symbol: String, spec: Specification ⇒ Bool.
first-invoked-in-body? symbol: String, spec: Specification ⇒ Bool.
invoked-symbols spec: Specification ⇒ {String}.
first-appearance symbol: String, spec: Specification ⇒ Nat.
bound-as-of? symbol: String, position: Nat ⇒ Bool.
next-chapter n: Nat ⇒ Nat.

invoked-symbols spec =
 [∀ chapter <: spec, head-s <: (chapter 0) ⇒ head-s] +
 [∀ chapter <: spec, body-s <: (chapter 1) ⇒ body-s].


Specifications can also be type-checked to ensure that your logic is consistent.

type-checks? expr: Expression ⇒ Bool.

(∀ expr <: expressions spec ⇒ type-checks? expr) → check spec.

expressions spec: Specification ⇒ [Expression].


Learn More

Pantagruel on GitHub

Pantagruel Language Reference

A Specification of a Note-Taking Program