Halis documentation

Halis is a secure, self-hosting, native-first systems language. This is the reference for the language, the effect system, the standard library and the toolchain.

Where to start

If you want to…	Go to
Run your first program	Getting started
Understand why a function is pure	Effects
See how untrusted input is handled	Taint tracking
Look up a type or a conversion	Types
Look up an effect, a builtin or a target	Quick reference
Follow a release	Releases

The three ideas

Halis rests on three ideas that everything else follows from.

Safety is the default, not an option. Integer overflow, division by zero and out-of-bounds access all halt safely. There is no switch that turns the checks off — the only way a check disappears is a formal proof that it is dead.

I/O is an effect, and effects must be declared. A function without a uses clause is guaranteed pure by the compiler — not by convention, not by review, by construction. The compiler walks the call graph and refuses to compile a function that reaches an effect it never declared.

Nothing hides. Every value carries an explicit type, there is no null, there are no globals, and hlc --audit prints the capability and taint-flow report of every function in the program.

The language in one file

import "std.sanitize"

struct Point {
    x: int,
    y: int
}

impl Point {
    fn dist2(self: Point) -> int {
        return self.x * self.x + self.y * self.y
    }
}

fn greet(name: str) -> str {
    return "Hello, " + name + "!"
}

fn main() -> int uses Args, IO {
    let p: Point = Point { x: 3, y: 4 }
    println("dist2 = " + p.dist2().to_str())
    println(greet("Halis"))

    # Command-line input arrives tainted; sanitise it before it reaches a sink.
    let argv: list[tainted[str]] = tainted_args()
    if argv.len() > 1 {
        println("hello, " + sanitize_filename(argv.get(1)))
    }
    return 0
}

greet has no uses clause, so the compiler proves it is pure: it cannot print, read a file, read the clock or touch the network. main declares Args and IO, and it pays for exactly those.

Specification

The frozen, normative reference is SPEC.md in the repository. It is the legal document for the project: the v1.0 API surface is pinned at a digest and hls-freeze refuses drift.

Note that SPEC.md is a historical document — it describes the language as it evolved, stage by stage. Where it disagrees with the shipped compiler, the compiler is right, and the quick reference is generated from the compiler source.