Magmide

Magmide is an open-source GitHub project that aims to create a programming language making formal verification and provably correct software practical and mainstream. The README describes it as a dependently-typed proof language intended to be to Coq what Rust has been to C. The repository is marked dormant while the author rethinks what the project could or should be, and it consists largely of notes, speculative writing, and exploratory theorem proving.

What It Is

Magmide is a design and research effort for a verification-oriented language aimed at working engineers rather than academics. It builds on proof assistant ideas such as Coq's Calculus of Constructions and on the Iris separation logic, which the README cites as able to verify complex, concurrent imperative code, including Rust code that uses unsafe. The README says the language should be capable of arbitrary logic, bare metal performance, gradual verification, reuse through metaprogramming, ergonomic tooling, and effective teaching material.

The Split Logic/Host Architecture

The planned design separates two languages. Logic is a dependently typed lambda calculus where types are defined and proofs are conducted. Host is the imperative language that runs on real machines. Logic defines and verifies Host, while Host represents and implements Logic. The bootstrapping plan is to build Magmide as the Logic portion with Rust as Host, define Rust's semantics within Magmide, and add a reflective proof rule so verified Rust code can be used during proof checking. Trackable effects, based on the Iron obligation logic, are planned to let some safety conditions stay optional while remaining visible.

Current Status

The README states the repo is dormant for now and still very early and rough. The repository contains exploratory Coq code in theory, a skeleton bootstrapping toolchain in Rust, OCaml and Coq, speculative essays in posts, and personal learning notes. It also includes a talk video and an FAQ covering design rationale, and it lists possible applications such as verified critical systems, secure voting protocols, and provable foundations for operating systems and databases.