Phil
A systems programming language in which the architecture — boundaries, protocols and proof obligations — is executable, and any implementation of it can be replaced.
Phil is a systems language built around the idea that architecture is executable and implementation is replaceable. Rather than defining a system by one implementation, it starts from system boundaries, protocols, authority and proof obligations, and lowers those meanings toward executable code.
Its development model is prototype, verify, rewrite, certify: proof is meant to cost at compile time, while uncertainty costs at runtime, and assurance machinery is erased once it has done its job. The project documents itself through a tutorial called A Tour of Phil, a frozen historical worked example called the Phase 0 framed-upload tour, and a keyword lexicon for its Grammar-v1 reserved words. Phase 0 is frozen as the first complete design and execution snapshot, and Phase 1 is active development that is removing Phase 0's witness-specific assumptions.
It has a focused, polarized, intuitionistic substructural dependent type system, and is released under the Apache-2.0 license.