Navid

Posted on Apr 6

Spectrelang - A design by contract programming language built for correctness and low-level control

#programming #softwaredevelopment #softwareengineering #opensource

Repository: https://github.com/spectrelang/spectre

It is often the case that low-level programming suffers from a tension between performance and safety. Languages such as C offer control though provide little protection, others add safety but often at the cost of explicitness, predictability, and performance.

Spectre is a solution that aims to resolve that by making correctness itself a first-class feature of the language.

What is Spectre?

Spectre is a contract-based, systems-level programming language designed around formal verification.

Rather than treating correctness as an afterthought (tests, linting, runtime checks), Spectre bakes it directly into the language through preconditions, postconditions, invariants, and explicit trust boundaries.

The result is code that is fast, low-level, self-documenting, and provably correct by design.

Core Philosophy

Safety by Contract

Every function defines what it expects and what it guarantees.

fn divide(a: i32, b: i32) i32 = {
    pre {
        not_zero: b != 0
    }

    val result = a / b

    post {
        is_scaled: result <= a
    }

    return result
}

Preconditions must hold before execution
Postconditions must hold before returning

If any contract fails in debug builds, the program halts safely.

Explicit Trust

Spectre introduces the idea that trust is visible in the type system.

fn print_data() void!

The ! in this case means: "This function cannot be formally verified."

This typically applies to:

I/O
FFI calls
Low-level memory operations

Trust Propagation

If you call unverified code, you must acknowledge it:

pub fn main() void! = { // Note how this is marked as '!'
    do_some_thing()
}

Or explicitly override through use of the trust keyword, like so:

trust std.stdio.puts("hello world")

This prevents hidden unsafety from creeping through a codebase.

Immutability by Default

Everything is immutable unless you opt in:

val x: i32 = 10          // immutable
val y: mut i32 = 20      // mutable

Even struct fields respect this at the binding level, thus there are no accidental mutation leaks.

A Real Example: Verified Data Structure

A stack with enforced correctness:

pub fn (Stack) push(s: mut self, vl: i32) void = {
    pre {
        not_full: s.len < trust @capacity(s.data)
    }

    trust @append(s.data, vl)
    s.len = s.len + 1
}

pub fn (Stack) pop(s: mut self) option[i32] = {
    pre {
        not_empty: s.len > 0
    }

    val top = trust @get(s.data, s.len - 1)
    trust @remove(s.data, s.len - 1)
    s.len = s.len - 1

    return top
}

This means no more:

popping from empty stacks
overflowing buffers

These are guaranteed by construction, rather than by testing.

Compile-Time vs Runtime Verification

Spectre currently uses a hybrid model:

Runtime (today)

Contracts are lowered into runtime checks in non-release builds:

Compiled into branches
Failures trigger immediate program termination

Compile-time (future)

Planned features include:

Range analysis
Symbolic reasoning
Proof-based elimination of checks

Meaning, if something can be proven safe at compile time, it will be.

Option & Result Types

Spectre embraces explicit error handling:

fn can_fail(should_fail: bool) option[i32]! = {
    if (should_fail) {
        return some 10
    }
    return none
}

And richer error modeling:

pub fn add_two_strings(a: ref char, b: ref char) result[i64, ParseError]! = {
    val x = string_to_i64(a)?
    val y = string_to_i64(b)?
    return ok (x + y)
}

No exceptions or hidden control flow. Everything is explicit.

Pattern Matching & Unions

Tagged unions are first-class:

match x {
    Int32 a => { ... }
    Pair z, y => { ... }
    else => { ... }
}

Exhaustiveness and correctness are enforced by the compiler.

Low-Level Control (Without Giving Up Safety)

Spectre does not hide the machine in any capacity:

extern (C) fn my_malloc(space: usize) ref void! = "malloc"

Note here:

Full FFI support
Explicit unsafe boundaries (!)
Contracts still apply around unsafe code

Platform-Aware Code

Compile-time conditionals:

when linux {
    // Linux-specific code
}

when darwin {
    // macOS-specific code
}

Note how there is no preprocessor or macro required. Instead, we use structured, readable conditions.

Why Spectre Exists

Most languages fall into one of these categories:

Category	Problem
Low-level (C, C++)	Fast but unsafe
High-level	Safe but opaque
Rust, Ada, Modula-2	Safety exists, but correctness is still implicit

Spectre takes a different stance, in that correctness should not be inferred. It should be declared, enforced, and visible.

Direction

This is still early (v0.0.1), though the direction is:

Stronger compile-time verification
Smarter contract elimination
Better ergonomics around trust boundaries
A robust standard library built around correctness

DEV Community