Getting started

Install

Install Hull from the Chelis-Lang GitHub org using reef:

chelis reef install --from-github Chelis-Lang/hull@v0.1.7

Verify the installation:

chelis hull --version

Check a program against the spec

Pass a Deep source file to Hull's reference type checker:

chelis hull check myprogram.deep

Hull derives the type and effects of the program according to the formal typing rules, then prints the result. If the program is ill-typed under the spec, Hull reports the rule that fails and the subterm responsible.

Compare spec output against compiler output

Run the compiler's type checker and Hull's reference checker on the same file, then diff:

chelis check myprogram.deep > compiler.out
chelis hull check myprogram.deep > spec.out
diff compiler.out spec.out

Any difference indicates a divergence between the implementation and the specification. The same pattern works for evaluation:

chelis eval myprogram.deep > compiler.out
chelis hull eval myprogram.deep > spec.out
diff compiler.out spec.out

Disagreements in either direction are worth investigating: the compiler may have a bug, or the spec may need a correction.