Hull

Hull is the executable specification of the Chelis language. It defines the shape of the language: the typing rules, the operational semantics, and the boundary between well-typed and ill-typed programs. Where a traditional language spec lives in a PDF, Hull lives in Chelis itself.

Self-hosted executable spec

Hull is written in Chelis and type-checked by Chelis. It implements the formal typing rules and operational semantics as ordinary Chelis functions operating on ADT representations of the Deep AST. The Deep AST is homoiconic, so Hull operates directly on the same representation the compiler uses. There is no translation layer, no external metalanguage, no deserialization step.

Think of it as PLT Redex without an external language: the specification and the implementation share a single representation and a single type system.

Three capabilities

Hull provides three independent tools, each derived from the formal rules:

1. Reference type checker. Given a Deep program, Hull derives its type and effects according to the formal typing rules. Compare against chelis check to surface spec-implementation disagreements.

2. Reference evaluator. Given a well-typed Deep program, Hull reduces it step by step according to the operational semantics. Compare against chelis eval to surface semantic divergence.

3. Spec-driven test generation. Hull generates random well-typed Deep programs using the typing rules as constraints. Each generated program comes with its expected type from the reference checker. This gives conformance testing at the language level, not at the library level.

Why it matters

When the compiler and the spec disagree, one of them has a bug. Hull makes that disagreement observable and reproducible. It turns the spec from a document that humans read into a program that machines execute, diff, and fuzz.