A Most Learned Assistant for Rigorous Thinking

module HAIKU.

Poem = [Line].
Line = String.

scans? p: Poem ⇒ Bool.

A haiku is a poem of exactly three lines.

scans? p → #p = 3.

Each line has a prescribed number of morae; the numbers of morae go 5, 7, 5.

scans? p → morae (p 1) = 5
  ∧ morae (p 2) = 7
  ∧ morae (p 3) = 5.


A mora is like a syllable, but shorter; it is known in Japanese as 音. To evaluate a line we count its morae.

morae l: Line ⇒ Nat.

Pantagruel is a computer program designed to help human beings think and communicate rigorously.

The human thinker can write a description of some system of rules, propositions, or behaviours in Pantagruel’s syntax and the Pantagruel document checker will attempt to validate the description.

Pantagruel constrains the human thinker into some of the syntactic forms of first-order logic and computer programming. In doing so it is hoped that the thinker will encounter elements of their thought which require further precision.

Through some simple constraints on the introduction and use of terms, Pantagruel might be able to assist the thinker in eliminating certain kinds of ambiguity to which natural language is prone.

module CHECKOUT.

owner d : Document ⇒ User.

A specification for a small document management system.

check-out u:User, d:Document.

A user may check out a document if they have permission to access it and it’s not currently checked out.

owner d = nobody ∧ has-perm? u d → owner d′ = u.
owner d ≠ nobody ∨ ¬(has-perm? u d) → owner d′ = owner d.


nobody ⇒ User.
has-perm? u:User, d:Document ⇒ Bool.

Quick Start

Install Pantagruel from AUR

          yay -S pantagruel

Install Pantagruel from Source (requires the Janet language and package manager)

Clone the Pantagruel repository:

          git clone

Install dependencies:

          jpm --local deps

Build Pantagruel:

          jpm --local build

Move the pant application to your PATH:

          mv build/pant ~/bin

Learn More