Pantagruel: An Extremely Lightweight Specification Language

Thought.
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 semantics.

eval spec = Nil.

---

---

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.

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

---

---

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

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

invoked-symbols ⇐ {String}.
chapter head: Head, body: Body ⇒ Chapter.
first-appearance symbol: String ⇒ Nat.
bound-as-of? symbol: String, Nat ⇒ Bool.
next-chapter n: Nat ⇒ Nat.

---

invoked-symbols spec = {∀ s: String ⇒ s in spec}.