A DOS object linker that makes use of DPMI to be faster than LINK.EXE and handle larger binaries.
A protected-mode debugger for DOS.
Evolution of a (once) popular C and C++ compiler for DOS.
Non-standard libc extensions commonly used by DOS programs, for use with GCC targeting x86-16.
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.