Quick Start

Ligare is an experimental systems programming language and compiler written in Rust. Its core idea is simple: everything is a term, and every relationship between terms is a constraint.

The current repository includes a C backend, a standard library, package commands, a formatter, a Markdown documentation generator, and the ligls language server. The language is still evolving, so examples in this site describe the current implementation rather than a stability promise.

Build the compiler

From the compiler repository:

cargo build --release
cargo build -p ligls --release

When the compiler is run from that checkout, debug builds discover the bundled standard library automatically. For a release binary used elsewhere, set an absolute standard-library path:

export LIGARE_STD_PATH="/absolute/path/to/ligare/libs/std"
target/release/ligare --version

The C backend also needs a C99-compatible compiler available as cc, or through the CC environment variable.

Create a small program

Create a binary package and replace its generated entry file with:

use std::io::print_line

pub def main : IO () :=
  do
    print_line 42

Then check and run it:

ligare new hello
ligare check --manifest-path hello/ligare.toml
ligare run --manifest-path hello/ligare.toml

The program prints 42. A binary package uses src/main.lig by default and must expose pub def main : IO ().

Where to go next

• Terms and constraints explains the core language model.
• Data and functions introduces values, functions, and refinements.
• Enums and matching covers sum types and elimination.
• Proofs and tactics explains checked proof construction.
• The ligare command lists source and package workflows.
• The standard library lists the modules shipped in libs/std.