A Record of the Proceedings of SIGBOVIK 2015 (PDF).

Your kids will love a cookie-decorating party, by Mark Dominus. Recommended reading.

Lean is a new open source theorem prover being developed at Microsoft Research, and its standard library at Carnegie Mellon University. Apache 2.0 licensed. Contains a library for Homotopy Type Theory.

Our Favorite Typefaces of 2014, by Typographica.

WhyTheName of your favourite Unix tool.

xNBD is yet another NBD (Network Block Device) server program, which works with the NBD client driver of Linux Kernel.

Scan Tailor is an interactive post-processing tool for scanned pages. It performs operations such as page splitting, deskewing, adding/removing borders, and others.

lua-ed, an implementation of the standard Unix editor “ed”, written in Lua.

1401 - FORTRAN Illustrated, “an innovative 63-pass compiler that ran in only 8k of core.”

formal-morality, a formal moral framework coded in Haskell.

Is It O.K. To Be A Luddite? (1984), by Thomas Pynchon.

The US Forest Service’s Cocktail Construction Chart

Tiling by Squares, a whole website about it.