Albite
formerly Tungsten by Spinning Cat Studios
A dependently typed language that proves what it computes. Write programs and the theorems about them in one language, and let the compiler check both.
-
Types that say what you mean
Algebraic data types, generics and dependent types, with structural recursion checked for termination.
-
Proofs beside programs
State a theorem about a function in the same file, prove it by tactic or by term, and a small kernel re-checks every proof.
-
Native code
Programs compile through LLVM to a static binary, and the compiler is written in the language it compiles.
-
Diagnostics you can ask about
Every error code has an explanation on the command line, and the inspection tools show what each definition elaborated to.
The compiler checks the claim
The type of _p says that a one-element list has length 1, for every n. The compiler evaluates
length to decide it, and the program does not build if the claim is false.
type List = Nil | Cons(Nat, List)
fn length(l: List) -> Nat {
match l {
Nil => 0,
Cons(h, t) => 1 + length(t),
}
}
fn length_of_one(n: Nat) -> Unit {
let _p: Eq<Nat, length(Cons(n, Nil)), 1> = refl;
()
}Try it in your browser
The playground runs the compiler's checker in a Web Worker. Nothing to install.
Open the playgroundQuestions
- Is it ready for production?
- Not yet. The 2.0 releases are previews, and the roadmap says what is left.
- Do I need to know type theory?
- No. Start with ordinary programs; the proof features are there when you want them.