A Lisp that fits into a BIOS boot sector.
An optimizing back end and intermediate representation for compilers of functional languages that are based on graph reduction (such as Haskell, Agda, or Idris).
A compiler suite for C, Modula-2, and other languages targeting 8- and 16-bit CPUs.
In addition to many low-end processors, also targets the VideoCore IV, the VPU on the original Raspberry Pi.
A GNU/Linux-like operating system and kernel for x86-16.
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.