Sabline in an hour

Sabline is a language where a function's first line tells you everything: what it takes, what it gives back, what it is allowed to touch, whether it can fail, and what it promises about its answer. Those promises are checked by a theorem prover before your program runs.

You can follow along in the browser — the playground runs the real compiler — or install it:

pip install sabline-lang
sabline doctor
sabline new hello && cd hello && sabline main.vel

1. Hello #

fn main() uses io {
    print("hello!")
}

main is where a program starts. uses io is a declaration: this function is allowed to talk to the outside world. Remove it and the program will not compile, because print needs it.

That is the whole idea of Sabline in one line — abilities are declared, not assumed.

2. Values and types #

fn main() uses io {
    let name = "Gowri"           // Text
    let age = 30                 // Int
    let ratio = 1.5              // Float
    let happy = true             // Bool
    let scores = [10, 8, 9]      // List of Int
    let ages = {"a": 1, "b": 2}  // Map of Text to Int
    let fee = money(1250, "INR") // Money of INR - 12.50, as 1250 paise
    print(format("{} is {}", name, age))
}

Types are inferred for locals and written down for parameters. Numbers do not mix silently: 1 + 1.5 is an error, because rounding surprises are how money goes missing. Convert on purpose with to_float(x) or round(x).

Actual money never becomes a Float at all: an amount is whole minor units with its currency in the type, two currencies never mix, and a division that could round says how (SPEC.md §4.3).

format fills each {} with a value, and the compiler counts the holes for you — the wrong number of values is a compile error, not a mess at runtime.

3. Functions and effects #

fn double(n: Int) -> Int {
    return n * 2
}

fn greet(name: Text) uses io {
    print("hello, " + name)
}

double is pure: no uses, so it cannot print, read files, or reach the network — and neither can anything it calls. The checker follows the whole call chain, so a pure function cannot sneak an effect in through a helper.

The effects are io, fs (files), net (network), clock (the time), and rand (randomness).

4. Promises, proven #

fn discount(price: Int) -> Int
    requires price >= 0
    ensures result >= 0
{
    return price - 10
}

requires is what the function needs from you. ensures is what it promises in return. Run this and the compiler answers:

error[E700] promise cannot be kept: 'discount' ensures result >= 0
  proven without running the program: price = 5 gives result = -5

It did not test the function. It proved the promise false and handed back the input that breaks it. Fix the code, or fix the promise:

fn discount(price: Int) -> Int
    requires price >= 0
    ensures result >= 0
{
    if price < 10 {
        return 0
    }
    return price - 10
}

Now it compiles, and sabline explain will say [proven].

Promises can talk about lists, maps, records and floats too:

fn bump(counts: Map of Text to Int, word: Text) -> Map of Text to Int
    ensures get_or(result, word, 0) == get_or(counts, word, 0) + 1
{
    return put(counts, word, get_or(counts, word, 0) + 1)
}

Floats are proven in real IEEE-754, which means Sabline will refuse to prove x + 0.1 + 0.1 == x + 0.2 — because on a real machine it is false. See docs/floats.md for why that matters.

5. Loops #

fn count_up(n: Int) -> Int
    requires n >= 0
    ensures result >= 0
{
    let total = 0
    let i = 0
    while i < n {
        total = total + 1
        i = i + 1
    }
    return total
}

No invariant line needed: the compiler works out the boring ones itself (each counter never goes below where it started). When you need something richer — "this total stays positive" — write it:

    while i < length(xs)
    invariant total >= 0
    {
        ...
    }

6. Failure #

Some things genuinely fail. In Sabline that is part of the signature, and ignoring it does not compile:

fn parse_age(t: Text) -> Int or fail {
    return try to_int(t)
}

fn main() uses io {
    check parse_age(ask("your age?")) {
        ok n {
            print(format("you are {}", n))
        }
        fail why {
            print(format("that was not a number: {}", why))
        }
    }
}

check handles it here. try passes it up to your caller (only inside a function that says or fail). The built-ins that fail in ordinary life — to_int, read_file, fetch, and get on a map — all say so, and get_or(m, key, default) is there when you would rather have a fallback than a failure.

7. Records and lists #

record Expense {
    what: Text
    amount: Int
}

fn describe(e: Expense) -> Text {
    return format("{}: {}", e.what, e.amount)
}

Records are immutable: Expense(what: "chai", amount: 25) makes one, e.what reads a field, and nothing can change it underneath someone. Lists work the same way — push gives you a new list.

Reading past the end of a list is caught before the program runs when the compiler can prove it, and reported cleanly when it cannot.

8. Function values #

import "std.vel"

fn main() uses io {
    let xs = [5, 3, 8, 1]
    print(keep_if(xs, fn(n: Int) -> Bool { return n > 4 }))
    print(sort_by(xs, fn(n: Int) -> Int { return -n }))
}

Inline functions are pure and cannot use variables from around them — pass what they need as parameters. They can carry their own promises, proven like any other function's.

9. Using libraries #

import "std.vel"                    // sort(xs), first(xs), join(...)
import "lib/geo.vel" as geo         // geo.distance(a, b)

A named import keeps a library's functions behind its own name, so two libraries that both define distance can be used in one file. The standard library is written in Sabline and keeps its own promises: sort carries ensures is_sorted(result).

10. The tools #

sabline program.vel                              # run it, with io and nothing else
sabline program.vel --allow io,fs:read:./data    # grant exactly that
sabline program.vel --allow all                  # every effect (it says so)
sabline migrate --to 5.0 .                       # the budget each program here needs
sabline check program.vel                        # compile it without running
sabline explain program.vel                      # what each function does, needs and promises
sabline explain .                                # the same for a whole project
sabline trace program.vel                        # watch every call as it happens
sabline repl                                     # try things, proofs and all
sabline fmt program.vel                          # canonical formatting
sabline doctor                                   # check your setup
sabline new myproject                            # start something
sabline build program.vel                        # one executable you can give to anyone
sabline add <url or path>                        # vendor a library into lib/
sabline verify                                   # check your libraries are unchanged

sabline explain is the one to reach for when you meet unfamiliar code: it lists every function with its effects, its promises, and whether those promises were proven or are being checked while running.

Where to go next #

• The language reference — what all of this means, precisely.

• examples/ledger.vel — an expense tracker: records, files, reports.

• examples/wordcount.vel — text analysis: maps, lambdas, failure.

• examples/fetcher.vel — an HTTP tool: the network, honestly declared.

• The error index — every message Sabline can give, scraped from the compiler itself.

If you can make the prover claim something is proven when it is false, that is a security bug and the project wants to hear about it.