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.
A dependently typed, imperative, bare-metal programming language.
Code manual (as in documentation) generator with Javadoc and OpenAPI integration.
The quite exquisite novel I read while on vacation.
Another take on a progressive consumption tax with many of the same benefits as the personal expenditures tax, except it treats capital gains as non-taxable. Apparently the math makes this work out the same in the end somehow, but it feels a little less politically viable (and obviously fair) to me.