A tutorial.
Cheap imperative data structures for Haskell. Even comes with NullPointerException support.
Haskell library for defining values recursively while avoiding nontermination. Magic.
A prelude extension for Idris. Contains many useful data types and algorithms.
Imports a variety of build systems into Nix.
Currently supports Rust, Haskell, PHP, Node.js, and Python.
A course on logic and proof theory using the Lean theorem prover.
Currently uses Lean 3, which is a bit different from Lean 4.
Added features:
- AArch64 support
- Parallel garbage collection
- Byte code mode
- Optimizations
Chinese and Japanese handwriting recognition engine.
An x86 Unix clone with a ’90s-style graphical user interface.
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.