Spectre is a statically typed, DbC programming language built for low-level control in combination with verifiably safe constructs.
It features 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 through the use of the guarded construct. More notably there is a type-level invariant system, wherein conditions in type invariants are evaluated at compile time.
Spectre compiles to QBE IR which lowers to assembly, though there are also experimental LLVM and C99 backends as per v0.0.5.
val math = use("std/math")
union Shape = {
Circle(f64) | Rect(f64, f64) | Triangle(f64, f64, f64)
}
fn area(s: Shape) f64 = {
match s {
Circle r => { return 3.14159 * r * r }
Rect w, h => { return w * h }
Triangle a, b, c => {
val sp = (a + b + c) / 2.0
return math.sqrt(sp * (sp - a) * (sp - b) * (sp - c))
}
}
}
/// 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
}
enum Status = {
Ok,
NotFound,
PermissionDenied
}
union Payload = {
i32 | i64 | ref char
}
fn describe(x: Payload) void! = {
match x {
i32 => { std.stdio.puts("32-bit integer") }
i64 => { std.stdio.puts("64-bit integer") }
else => { std.stdio.puts("string pointer") }
}
}
/// 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
}