Forem: Navid

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

Navid — Mon, 06 Apr 2026 16:29:04 +0000

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

Axelang - A Systems Programming Language with Concurrency as a First-Class feature

Navid — Fri, 21 Nov 2025 23:55:12 +0000

Axelang is a new systems programming language designed around the following question:

Why is concurrency an afterthought, a library, or a bolt-on runtime — as opposed to a language-level concept?

Axe aims to resolve the issue in that rather than forcing developers to manually struggle with bolted on threads, locks, futures and external libraries, Axe makes concurrency part of the core language semantics, in that writing Axe forces you to think concurrently by default.

Why Axe Exists

Modern CPUs have not been about single-thread speed for a long time. Performance improvements are generally achieved by:

Adding more cores
Adding more threads
Hiding I/O latency
Overlapping compute with work

But most languages still make concurrency:

verbose
error-prone
tacked on after the fact

C, C++, Java, and Rust rely heavily on APIs, libraries, and patterns. Go introduced goroutines, but concurrency is still a runtime abstraction — not part of the language type system. Concurrency should feel like a natural mode of thinking, not a box of add-on primitives.

Concurrency as a Language Construct

A simple Axe program might include:

main {
    parallel {
        single {
            task1();
            task2();
        }
        task3();
    }
}

This reads almost like pseudocode:

parallel {} introduces a parallel execution region
single {} means “one thread runs this block”
work-sharing and scheduling are handled by the compiler + runtime

Axe’s concurrency constructs are structured, visible in the syntax tree, easy for static analysis, and safe to optimize.

Instead of bolting on OpenMP-style pragmas, heavy macro systems, or attributes, Axe builds them directly into the grammar.

Platform-Aware Code at Compile Time

Axe also supports compile-time dispatch based on OS or platform:

platform windows {
    println "Running on Windows";
}
platform posix {
    println "Running on POSIX";
}

This allows the compiler to eliminate unused branches, generate smaller binaries, and avoid runtime platform checks.

Your code can remain portable without littering your project with #ifdef walls.

A Powerful Dispatch System… Without Generics

One standout feature is Axe’s compile-time overload map:

overload println(x: generic) {
    string => println_str;
    i32    => println_i32;
}(x)

This looks simple, but it’s extremely powerful:

Axe can resolve overloads statically
No generics required
No template instantiation explosion
No runtime dispatch cost
Works with user-defined types

This lets Axe provide generic-friendly ergonomics without introducing template systems or complex type parameterization.

Familiar, But Cleaner

Axe feels like a blend of:

C-style syntax
Go-like readability
Rust-level respect for correctness
Zig-style minimalism

But it doesn't copy any of them. Axe aims to be:

easier than C++
more predictable than Rust’s borrow checker
more explicit than Go
safer than straight C

If you know a systems language, you can read Axe code in minutes.

A Language Designed to Scale

Axe has:

models (its version of simple data types)
functions with clear signatures
compile-time branching (for platforms, modes, and toolchains)
parallel loops and reduction built in

Example parallel loop:

parallel for mut i = 0 to n reduce(+:sum) {
    sum = sum + i;
}

The compiler turns this into efficient work sharing, correct reduction handling, and thread safe execution.

It does not require a single pragma, library import, or thread API.

You can read more or try it at:

axelang.org