The Ligare Programming Language

Appearance

The Ligare Programming Language

Terms, constraints, proofs, and data in one small core

Start learning
Compiler source

Terms and constraints

Values, propositions, functions, and constraints share one term language.

Refinements and proofs

Express invariants with where clauses and discharge obligations with checked proof tactics.

Data that maps to C

Structs, enums, pattern matching, and effects are lowered by the current C backend.

Tooling that follows the compiler

The formatter, documentation generator, and ligls language server use the same language pipeline.