The Ligare Programming Language

Appearance

The Ligare Programming Language

Wellcome to the Ligare Programming Language

Begin
See on github

Everything is a term.

Types, proofs, and contracts are one thing.

Dependent types with zero cost.

Refinements and invariants compile to nothing.

Proofs you don't have to write.

The compiler does the obvious ones. You stay in control.

C where you need it.

Direct FFI, custom allocators, no runtime. Build anything from kernels to compilers.