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 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.
(all s <: invoked_symbols spec =>
	first_invoked_in_head? s spec -> bound_as_of? s (first_appearance s spec)
	and
	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 =
	[all chapter <: spec, head_s <: (chapter 0) => head_s] +
	[all chapter <: spec, body_s <: (chapter 1) => body_s].

;

Expression.

// Specifications can also be type-checked to ensure that your logic is consistent.
type_checks? expr: Expression => Bool.
---

(all expr <: expressions spec => type_checks? expr) -> check spec.

;

expressions spec: Specification => [Expression].
---