Charge

Charge is an experimental memory-safe systems programming language, most similar to C++ and Rust. It is a personal research project in early development. The primary goals of the language are:

• Proven memory safety … : rigorous and semi-automatic proofs, enabled by formalizing reference guarantees, object invariants and more in the project’s own intermediate representation Chiral.
• … that doesn’t get in the way: most code should not interact with the proof system directly. Writing manual proofs is the escape hatch from inherently safe borrow-checked semantics.
• Extensive proof system: advanced memory techniques and hacks that are possible in C++ should be possible in Charge too, when accompanied by a proof.
• Compact and powerful foundation: the language is built on few but general concepts, unifying aspects of both C++ and Rust.