✓ written by AI · used by AI
The language that proves your code.
Sond is written by AI and used by AI. Its compiler is an oracle: it proves every function's contract at compile time — and rejects any code it can't prove correct.
curl -fsSL https://sond.dev/install.sh | bash
// abs never returns a negative number,
// and the compiler PROVES it.
fn abs(x: i64) -> (r: i64)
ensures { r >= 0 }
{
if x >= 0 { x } else { 0 - x }
}The compiler is the oracle.
Every function can carry a contract. sondc proves it against the
body at compile time. A contract it cannot prove is a compile error — not a runtime
surprise, not a failing test you forgot to write.
// abs never returns a negative number.
fn abs(x: i64) -> (r: i64)
ensures { r >= 0 }
{
if x >= 0 { x } else { 0 - x }
}// Same promise, wrong body: x can be negative.
fn abs(x: i64) -> (r: i64)
ensures { r >= 0 }
{
x
}error: postcondition not proven
--> abs.snd
| ensures { r >= 0 }
| ^^^^^^^^ the prover cannot show this holds for every input
= note: when x < 0, r = x < 0Divide-by-zero is a compile error
Sond proves the divisor is non-zero before it lets you divide. No runtime crash, no defensive check you might forget.
// ✗ rejected: divisor not proven non-zero
fn ratio(a: i64, b: i64) -> i64 {
a / b
}
// ✓ accepted: precondition proves b != 0
fn ratio(a: i64, b: i64) -> (r: i64)
requires { b != 0 }
{
a / b
}Illegal states don't compile
A value that might be absent is an Option. The only way to read it is
match, which forces you to handle the empty case. The billion-dollar
mistake — forgetting to check for absence — is unrepresentable.
enum Opt { Some(i64), None }
// Can't divide by zero: returns None.
pub fn safe_div(a: i64, b: i64) -> Opt {
if b == 0 { None } else { Some(a / b) }
}
// You must handle None to reach the value.
pub fn unwrap_or(o: Opt, fallback: i64) -> i64 {
match o {
Some(x) => x,
None => fallback,
}
}From contracts to bare metal
Sond has no interpreter. sondc emits native x86-64: a hosted ELF, a
freestanding libc-free /init, or a UEFI application that boots on bare
hardware with no OS underneath — the same proven language, all the way down.
Verified in QEMU/OVMF all the way through ExitBootServices into a
bare-metal kernel talking to COM1.
$ sondc app.snd -o app # hosted ELF
$ sondc init.snd --freestanding # libc-free /init
$ sondc boot.snd --uefi # BOOTX64.EFI — bare metalWritten by AI, used by AI
When AI writes at full speed, the bottleneck moves from writing to verifying. So the human writes and approves contracts; the AI fills in and proves the bodies; the compiler is the oracle in a tight loop.
The whole language is stress-tested by having a deliberately weak model write Sond programs that must compile — and, for verifiable outputs, run and check against known answers — before they ship.
“A language so hard to write that no human will use it — but when an AI writes in it, it never has to come back to fix a bug later.” — the Prime Directive
Install Sond
No root required. Installs sondc, the standard library, and
the language reference.
curl -fsSL https://sond.dev/install.sh | bash
curl -fsSL https://sond.dev/install.sh -o install.sh
less install.sh # read it before you run it
bash install.sh
git clone https://github.com/fredyk/sond
cd sond
cargo build --release --manifest-path compiler/Cargo.toml
tools/install.sh
Installs sondc to ~/.local/bin, the standard library to
~/.local/lib/sond, and the language reference Sond.md to
~/.local/share/sond. Requires git and a Rust toolchain
(cargo). Then: man sondc · man sond ·
language reference.
Open source. Real compiler. Active development.
A real compiler in Rust, built bottom-up with strict TDD: a linear-arithmetic prover with
path-sensitive branches, inter-procedural contract summaries, and loop invariants. Sum types
with Option/Result. Three native backends.