On the overapplication of intuitionism.
It rings true to me that classical logic is philosophically underappreciated. In most of mathematics, constructivism does not, I feel, carry its weight. On the other hand computation is intrinsically tied to intuitionistic logic, so it is important to know when one needs to apply it.
An innovative proprietary (possibly patented) logic that can prove your propositions extraordinarily efficiently.
A Linux kernel security module that enables applications to limit their own privileges.
You could use Seccomp filters directly, but do you really want to?
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.