A language for verified low-level software.
It dreams to be something like Rust with logic
― a language that empowers people to build verified low-level software.
The name Vel stands for various concepts.
Vel is a language for verified low-level software.
Vel commits to the velocity of both development and runtime.
Vel wants to be smooth and relaxing like velvet.
Vel features a dependent ownership type system.
It enables reasoning about runtime objects using some propositions.
Some propositions are copyable (like Rust's Copy), but others are not ― as we are in separation logic!
We can also use Rust-like borrows for sharing, very unlike traditional separation logic.
vel: Vel's language engine, written in Rust.vel-vscode: VS Code extension for Vel.