An introduction to langauge-oriented programming using Racket by Matthew Butterick.
A reproduction of Oliver Byrne’s celebrated work from 1847 plus interactive diagrams, cross references, and posters designed by Nicholas Rougeux.
A wiki-lab for collaborative work on Mathematics, Physics and Philosophy.
An introduction to programming language theory using the proof assistant Agda.
The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant.
A series creates a small operating system in the Rust programming language.