Normalization for Cubical Type Theory, by Jonathan Sterling and Carlo Angiuli. “We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory.”

Let’s Not Dumb Down the History of Computer Science, by Donald E. Knuth.

Schizophrenia in Contemporary Mathematics (PDF, 1973), by Errett Bishop.

BundleWrap is a decentralized configuration management system that is designed to be powerful, easy to extend and extremely versatile.

Counsel, a collection of Ivy-enhanced versions of common Emacs commands. counsel-rg and counsel-fzf are awesome!

QSCM: A Smooth Blend of Scheme and C, by Quentin Carbonneaux.

How does clang 2.7 hold up in 2021?

You Could Have Invented Homology (YouTube), by Boarbarktree.

An Incredible 10-Gigapixel Scan of ‘Girl With a Pearl Earring’

See a salamander grow from a single cell

The 27th IOCCC winners are up.

RISC-V Powered BeagleV Board Announced Via New Collaboration, featuring a dual core 64-bit U74 RISC-V CPU clocked at 1.5 GHz and up to 8GB of LPDDR4 RAM.

Perceus: Garbage Free Reference Counting with Reuse, by Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen. “Much like tail-call optimization enables writing loops with regular function calls, reuse analysis enables writing in-place mutating algorithms in a purely functional way. “

The G-machine In Detail, or How Lazy Evaluation Works

PlanckForth: Bootstrapping an Interpreter from Handwritten 1KB Binary

A guide to running IRIX 6.5.22 in MAME

Tongue-rolling: The myth, wrong things you learned in school.

FedEx Shipping Damage Creates Fractured Artworks

Lean Together 2021: An overview of Lean 4 (YouTube), by Leonardo de Moura and Sebastian Ullrich. The new syntactical features look really awesome.

Logical Verification 2020–2021, course held by Jasmin Blanchette and Gabriel Ebner. All material online. Uses Lean and the book “The Hitchhiker’s Guide to Logical Verification”.

Advent of Code 2020 solutions in Lean 4, by Reid Barton.

A Side Journey to Titan: Side-Channel Attack on the Google Titan Security Key, by Victor Lomne and Thomas Roche.

Plaintext HTTP in a Modern World, Joshua Stein on the Upgrade-Insecure-Requests header.

Ditherpunk – The article I wish I had about monochrome image dithering, by Surma.

Working off-grid efficiently, by Rekka Bellum.

Nicaraguan Sign Language is a sign language that was largely spontaneously developed by deaf children in a number of schools in Nicaragua in the 1980s.

A 11x11 Latin word square, by Eric Tentarelli.

Ray Tracing in pure CMake, whyyyy.

GANsky

Untold Dylan, “Almost 2000 articles and nearly 9000 comments on Bob Dylan including reviews of 621 songs that Bob Dylan has written.” (Frighteningly good.)

Cedille is an interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Curry-style) type theory.

What is the combinatory logic equivalent of intuitionistic type theory? (2012), well explained by Conor McBride.

GGP, EGP and 25 years of BGP: a brief history of internet routing (2016), by Iljitsch van Beijnum.

Rehabilitating Asynchronous Communication with NNCP: A Cross Between Tor, ssh, and UUCP, by John Goerzen. Also see followup posts.

The Design of the Roland Juno oscillators

Letter of Recommendation: Sleep, ‘Dopesmoker’ (2016). Best music review ever?