Open-sourced at last.
A DOS-related web forum.
An x86-family (x86-16, x86-32, x86-64) assembler.
Includes DMMI (DOS Multicore Mode Interface), which is a way to access DOS from long mode.
The full tutorial is also available as a separate article.
A 64-bit DOS extender. (See also.)
A DOS stub loader for 64-bit PE executables. (See also.)
Refinement types and correctness proofs for Haskell.
The Leftpad function, implemented and proven correct in various different proof and programming languages.
A model checker for Rust.
Static verification of function pre- and post-conditions for Rust.
Not as powerful as full dependent types, but could be a good middle ground between something like ATS and down-to-earth plain Rust.
A Java library for defining JMeter performance tests.
An imperative programming language for verified bare-metal programming. Currently targets RISC-V only.
A dependently typed domain-specific language for hardware design, embedded into Agda.
A low-level, dependently typed, impure functional programming language.
A language for verified hard real-time stream processing embedded into Haskell.
An imperative language for safe systems programming embedded into Haskell.
A dependently typed functional programming language where all data is unboxed by default.
Software Foundations in Idris instead of Coq.
A book series on the mathematical foundations of computing, formalized in Coq.
A C++-like programming language.
I donβt care for the language, but the name is hilarious.
A constructed natural language that is also a programming language.
A programming language and theorem prover, designed to be approachable to programmers and mathematicians alike.
Dependently typed programming language without garbage collection.