Spectre Programming Language

Built around verifiable behaviour

Spectre is a statically typed, contract-based programming language built for low-level control in combination with verifiably safe constructs. It has no garbage collector, and aims to deliver predictable performance.

Its distinguishing feature is a contract system integrated into the language grammar. Functions carry named preconditions and postconditions that participate in compilation and, depending on their form, in the generated binary. The programming language offers explicit control over which checks survive into release builds.

arena allocator with guarded precondition

/// Allocate `size` bytes from the arena.
pub fn (Arena) alloc(arena: self, size: usize) option[ref void] = {
    guarded pre {
        pre_size_positive : size > 0
    }
    val off: mut usize = trust @load(@ptradd(arena, 8))
    val cap: usize     = trust @load(@ptradd(arena, 16))
    val aligned: usize = (size + 7) - ((size + 7) % 8)
    if (off + aligned > cap) {
        return none
    }
    val buf: mut ref void = trust @load(arena)
    val ptr: ref void     = trust @ptradd(buf, off)
    trust @store(@ptradd(arena, 8), off + aligned)
    return some ptr
}

pre/postconditions and guarded checks

/// Return bytes remaining. Subtraction is safe because used <= cap.
pub fn (Arena) remaining(arena: self) usize = {
    pre {
        used_le_cap : trust @load(@ptradd(arena, 8)) <= trust @load(@ptradd(arena, 16))
    }
    val off: usize = trust @load(@ptradd(arena, 8))
    val cap: usize = trust @load(@ptradd(arena, 16))
    post {
        result_le_cap : off <= cap
    }
    return cap - off
}

enums, unions, and exhaustive matching

enum Status = {
    Ok,
    NotFound,
    PermissionDenied
}

union Payload = {
    i32 | i64 | ref char
}

fn describe(x: Payload) void! = {
    match x {
        i32  => { std.io.put("32-bit integer") }
        i64  => { std.io.put("64-bit integer") }
        else => { std.io.put("string pointer") }
    }
}

guarded precondition on public API boundary

/// Open a file; mode must be non-empty in all build configurations.
pub fn open(path: ref char, mode: ref char) option[ref void] = {
    guarded pre {
        mode_nonempty : mode != ""
    }
    val f: ref void = trust fopen(path, mode)
    if f == none { return none }
    return some f
}