/
Search
EN

Why kola?

kola is a systems language for the software underneath everything else: kernels, drivers, daemons, protocol stacks, network services. It has no garbage collector and compiles to native code. What sets it apart is the function signature. A kola signature states what the function can touch: which memory, which parts of the outside world, what it expects from its caller and what it promises back. The compiler checks every one of those claims, so one line tells a reviewer most of what they need to know.

Why another language?

Rust, C and Zig were all designed when writing code was the expensive part of the job, and they spend their design budget on the person writing it. That has changed. A first draft is now often produced by a model in seconds, while reading it, checking it and deciding whether to trust it still takes as long as it always did. kola spends its budget on that second person: the reviewer, the auditor, whoever maintains the code next year.

Safety is part of the result, but it is not the goal in itself. The goal is that you can accept code you did not write (a generated patch, a library, a colleague's module) after a cheap, mechanical check instead of a line-by-line read. The language provides five things for that:

  • Memory safety without a GC or a borrow checker. Memory lives in regions, and a reference typed by its region cannot outlive it. See Memory: regions and references.

  • Leaks are compile errors. A file, a socket or a transaction is a resource, and a resource has to be consumed on every path through the function. See Resources and linearity.

  • Access to the world is in the signature. Effects say what kind of thing a function does. Capabilities say what it does it to. A function that was never handed a network capability cannot open a socket. That is a property of the type system, not a coding convention. See Effects and capabilities.

  • Contracts cannot be switched off. A contract (req, ens) is either proven at compile time, in which case it costs nothing, or checked at run time. No release mode drops it. See Contracts, traps, and tests.

  • Every failing test replays from one number. Time, randomness and scheduling all flow through capabilities, and the test runner swaps them for seeded simulations. A red test prints its seed, and that seed reproduces the run exactly.

Why not a linter for Rust? Because each of these is a type rule enforced at every call boundary, including inside libraries you never opened. A linter can be skipped and a convention can be broken; a kola signature cannot. And although the language was shaped with generated code in mind, it is small, its syntax is close to Rust, and it is perfectly pleasant to write by hand.

Modern models also make it cheaper to search for vulnerabilities at scale. kola's response is to make the security-relevant surface of a program a finite list that a defender can check completely. That argument has its own page: Security: exhaustive defense against scalable offense.

Bug classes the language rules out

Bug class

What rules it out

use-after-free, dangling pointers

A reference carries its region in its type and cannot outlive it. Violations are compile errors.

double free

There is no free. A region is released as a whole, exactly once, at its closing brace.

leaked file, lock or transaction

Linearity: a resource must be consumed on every path.

null dereference

There is no null. A value that may be absent has type Option[T].

silent overflow, undefined behaviour

Arithmetic traps on overflow. Wrapping is written explicitly (+%). Nothing in the language is undefined.

out-of-bounds access

Every index carries a bounds contract that is either proven or checked, never skipped.

hidden access to network, disk or time

There are no global functions that reach the world. Every such operation needs a capability passed in explicitly.

data races

Threads share no mutable memory. Ownership moves between threads and references never cross, so a race cannot be written (see Threads and channels).

There is one deliberate exception to the "no ambient authority" rule, and you meet it in the first program you write: the log effect needs no capability. Any function can say something. This does not open a hole, because the log sink is chosen once by whoever starts the process (kola --log, KOLA_LOG) and is write-only. The program cannot pick a destination and cannot read anything back, so logging cannot steer control flow or smuggle authority. Producing output, meaning bytes that another program will parse, is a different channel and does need a capability: sys.stdout.write(&bytes).

What it looks like

Here is a function that inspects untrusted bytes. The logic is deliberately naive: it counts zero bytes and flags the input if more than a quarter of it is zeros. The interesting part is the signature. Hover over the highlighted pieces:

enum Verdict { Clean, Suspicious }

pub fn scan[r](payload: &r [u8]) -> Verdict !{} {
    let mut zeros = 0;
    for i in 0..payload.len {
        if payload[i] == 0 { zeros = zeros + 1; }
    }
    if zeros * 4 > payload.len { Verdict::Suspicious } else { Verdict::Clean }
}

The signature has already answered the reviewer's main questions. scan receives no capability and is declared pure. If its body were rewritten by an attacker, or generated with a bug, it still could not send data anywhere, allocate memory or hang. What remains to review is the logic itself.

Here is the same code as a complete program. main receives the whole authority of the process and decides how much of it each callee gets. In this program neither callee gets any:

use std::log;

enum Verdict { Clean, Suspicious }

pub fn scan[r](payload: &r [u8]) -> Verdict !{} {
    let mut zeros = 0;
    for i in 0..payload.len {
        if payload[i] == 0 { zeros = zeros + 1; }
    }
    if zeros * 4 > payload.len { Verdict::Suspicious } else { Verdict::Clean }
}

// Logging is an effect, not a capability: the sink is write-only
// and chosen by whoever started the process.
fn report(v: Verdict) !{log} {
    match v {
        Verdict::Clean => log::info("payload: clean"),
        Verdict::Suspicious => log::info("payload: suspicious"),
    }
}

fn main(sys: Sys) -> u8 !{io, block, alloc(heap), log} {
    region r {
        let good = alloc in r [1u8, 2u8, 3u8, 4u8];
        let bad  = alloc in r [0u8, 0u8, 7u8, 0u8];
        report(scan(good));
        report(scan(bad));
    }
    0
}

When a callee does need something, you pass it exactly that and nothing more. This is called attenuation, and it is the entire mechanism. There is no permission file to maintain; the arguments you choose to pass are the policy:

use std::log;

// Receives the clock and nothing else. It cannot open a socket,
// read a file or allocate, because it holds nothing to do it with.
fn stamp(clock: &Clock) -> u64 !{io} {
    clock.now()
}

fn main(sys: Sys) -> u8 !{io, log} {
    log::info(f"t = {stamp(&sys.clock)}");
    0
}

Memory is budgeted the same way:

fn main(mut sys: Sys) -> u8 !{io, block, alloc(heap)} {
    let small: Mem = sys.mem.split(1048576);  // take 1 MiB from the root budget
    region r from small {                     // this region's arena draws on it
        let v: &r mut Vec[u64] = alloc in r mut Vec::new();
        v.push(1);
    }                                         // r is closed and its memory returned
    sys.mem.absorb(small);                    // give the budget back
    0
}

Two details matter here. split and absorb both modify the root bundle, which is why main takes mut sys; leave out the mut and the compiler tells you so. And Mem is one of the few capabilities you are not allowed to drop. Dropping an authority token such as Clock loses nothing, so the runtime reclaims it. A budget is a quantity, and losing it would be a real leak, so linearity makes you return it on every path.

As a result, a component's memory budget becomes part of its interface. How much memory a library needs is written in its code and in its package manifest. You do not find out from an OOM in production.

Where kola comes from

The name stands for kore language. kola is developed by Kore Ltd for its own systems work: a hypervisor, a filesystem, a database and the services around them. We needed a language that is safe, fast, checkable and small, and whose programs have clear, explicit boundaries. Contributions are welcome. We ask one thing of contributors: keep that idea intact.