Finite-Choice Logic Programming, by Chris Martens, Robert J. Simmons, and Michael Arntzenius. “We propose a new formalism, finite-choice logic programming, that uses choice, not negation, to admit multiple solutions. Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain.”

Optimality of Gerver’s Sofa, by Jineon Baek.

On “Safe” C++, by Isabella Muerte. What a ride.

Way too many ways to wait on a child process with a timeout, by Philippe Gaultier.

Some surprising code execution sources in bash

Chawan, a web browser for your terminal. Looks very decent already!

ad, an adaptable text editor in the spirit of Acme.

linotype.wiki, home to information about typesetting machines.

Resurrection, the Computer Conservation Society’s Journal.

Mathematische Schülerbücherei der DDR, 138 Bücher neu geTeXt, darunter “Köpfchen, Köpfchen”.

The December Adventure is low key. The goal is to write a little bit of code every day in December.

Nachruf auf Lothar König: Pfarrer und Punk, 1954–2024.

GIMPS Discovers Largest Known Prime Number: 2^136,279,841-1, first new Mersenne Prime found using GPUs.

Formalising Graphs with Coinduction, by Donnacha Oisín Kidney and Nicolas Wu (POPL 2025). “We argue in the paper that graphs are naturally coinductive, rather than inductive, and that many of the problems with graphs in functional languages go away once you give up on induction and pattern-matching, and embrace the coinductive way of doing things.”

The Design of a Self-Compiling C Transpiler Targeting POSIX Shell, SLE 2024 paper by Laurent Huberdeau, Cassandre Hamel, Stefan Monnier, and Marc Feeley.

getopt() but smaller, neat version by Tony Finch.

“Reflections on Trusting Trust”, but completely by accident this time, by duk.

Neural Networks (MNIST inference) on the “3-cent” Microcontroller, a PMS150C.

A line map for Milano’s trams in TeX, by terru.

Better-performing “25519” elliptic-curve cryptography, from AWS. With correctness proofs of the assembly code(!) in HOL/Light.

FreeBSD 11.0+ Kernel LPE: Userspace Mutexes (umtx) Use-After-Free Race Condition, detailed write up at Access Vector.

Unbindable Kemmy Schmidt, by Sophie Schmieg.

Can Logic Programming Be Liberated from Predicates and Backtracking? (PDF), by Michael Hanus.

A Mathematical Model of Package Management Systems, by Gershom Bazerman, Emilio Minichiello, and Raymond Puzio.

A liveness example in TLA+, by Lorin Hochstein.

Unsynchronized PPS Experiment, Josef “Jeff” Sipek improves NTP quality a lot with a $5 OCXO.

How do archivists package things? The battle of the boxes

Amazon S3 now supports conditional writes, finally!

The TESCREAL bundle: Eugenics and the promise of utopia through artificial general intelligence, by Timnit Gebru and Émile P. Torres. “T]hhe acronym “TESCREAL” denotes “transhumanism, Extropianism, singularitarianism, (modern) cosmism, Rationalism, Effective Altruism, and longtermism”.

A low-level look at A-normal form, by William J. Bowman.

SQL Has Problems. We Can Fix Them: Pipe Syntax In SQL, by Jeff Shute, Shannon Bales, Matthew Brown, Jean-Daniel Browne, Brandon Dolphin, Romit Kudtarkar, Andrey Litvinov, Jingchi Ma, John Morcos, Michael Shen, David Wilhite, Xi Wu, and Lulan Yu. Seems like a decent idea.

The GhostWrite vulnerability affects the T-Head XuanTie C910 RISC-V CPU. “This vulnerability allows unprivileged attackers, even those with limited access, to read and write any part of the computer’s memory and to control peripheral devices like network cards.”

Debugging a rustc segfault on illumos, by Rain.

SKINT is a portable interpreter for the R7RS Scheme programming language.

GLIM is a set of GRUB configuration files to turn a simple memory stick into being able to boot many Linux live environments.

Typical, data interchange with algebraic data types. “Typical can be compared to Protocol Buffers and Apache Thrift. The main difference is that Typical has a more modern type system based on algebraic data types, emphasizing a safer programming style with non-nullable types and exhaustive pattern matching.”

GCRA: leaky buckets without the buckets, by Tony Finch. An easy way to do rate-limiting.

rpdf makes working with PDF annotions super easy! It can merge annotations from multiple files, some show statistics (stats) or strip specific (or all) annotations.

Stitch is a minimal grep-based CLI note-managing system.

Yon is a little UI for knowledge, using a Acme-like interface in the Browser.

Planning Weekly Workouts in 100 lines of Haskell, by Rodrigo Mesquita.

The Dying Computer Museum, by Jason Scott.

How good can you be at Codenames without knowing any words?, by Dan Luu.

Against XMPP+OMEMO, by Soatok.

rtex is a reimplementation of TeX82 in Rust.

DECstation 2040, a RP2040 based DECstation 3000 emulator that can run DECWindows.

μLA: Micro Logic Analyzer, a SUMP/OLS compatible logic analyzer firmware for RP2040 based boards.

PiGFX is a bare metal kernel for the Raspberry Pi that implements a basic ANSI terminal emulator with the additional support of some primitive graphics functions. It can be driven by pushing characters to the Raspberry Pi UART.

Abstract interpretation in the Toy Optimizer, by Max Bernstein.

Revisiting Coroutines (PDF, 2004), by Ana Lúcia de Moura and Roberto Ierusalimschy. “This paper defends the revival of coroutines as a general control abstraction. After proposing a new classification of coroutines, we introduce the concept of full asymmetric coroutines and provide a precise definition for it through an operational semantics.” Recommended!

How to Share a Secret, Infinitely (2016), by Ilan Komargodski, Moni Naor, and Eylon Yogev. “In this work we consider the case where the set of parties is not known in advance and could potentially be infinite.”

Iconography of the X Window System: The Boot Stipple, by Matt T. Proud.

The bizarre secrets I found investigating corrupt Winamp skins, by Jordan Eldredge.

The Busy Beaver Challenge, “We have achieved our goal of proving ‘BB(5) = 47,176,870’”. Formally verified in Coq.

regreSSHion: RCE in OpenSSH’s server, on glibc-based Linux systems (CVE-2024-6387), a Qualys Security Advisory.

XAES-256-GCM is an authenticated encryption with additional data (AEAD) algorithm with 256-bit keys and 192-bit nonces. By Filippo Valsorda.

A Non-Terminating Game of Beggar-My-Neighbor, by Brayden Casella, Philip M. Anderson, Michael Kleber, Richard P. Mann, Reed Nessler, William Rucklidge, Samuel G. Williams, Nicolas Wu. “The existence of this non-terminating game provides a solution to a long-standing question which John H. Conway called an ‘anti-Hilbert problem.’”

On Understanding Data Abstraction, Revisited (PDF, 2009), by William R. Cook. Recommended reading. “An essential observation is that object interfaces do not use type abstraction: there is no type whose name is known but representation is hidden.”

Life in Johnstone’s Topological Topos, by Chris Grossack.

A Proof of Proof by Infinite Descent, by Ron Garcia.

Coccinelle for Rust implements semantic patches for Rust code.

Pirate Solitaire, by Victor Pernet.

Lynn Conway (1938–2024)

POSIX.1-2024 has been published!

Oregon Programming Languages Summer School 2024, videos and lecture notes are up!

Will we continue scientific research? (1972), by Alexander Grothendieck. Translated by Peio Borthelle.

A Machine-Checked Correctness Proof of Normalization by Evaluation for Simply Typed Lambda Calculus (PDF, 2017), by András Kovács.

Beyond the wall: Working with aperiodic tilings using finite-state transducers, by Simon Tatham.

The Gilbert–Johnson–Keerthi algorithm explained as simply as possible.

SIGMOD Programming Contest Archive, “SIGMOD hosts a yearly competition to design a system which performs a set of queries as quickly as possible. The contests provide a starting framework and test harness. They make great intermediate database projects for learning.”

PID 0 in V1 UNIX (and V4 nsys, and the PDP-7 proto-UNIX), by наб.

Apotris is a multiplatform open-source block stacking game.

Forsp, a Forth+Lisp Hybrid Lambda Calculus Language

Nokja Original, Classic 3310 Cellphone Font.

Principia Mathematica as a map.

A potpourri of cool-looking scripts

Your API Shouldn’t Redirect HTTP to HTTPS, by jviide.

A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem, by Ariel Kellison. “A direct proof of the Steiner-Lehmus theorem has eluded geometers for over 170 years.”

Assessing Game Balance with AlphaZero: Exploring Alternative Rule Sets in Chess, by Nenad Tomašev, Ulrich Paquet, Demis Hassabis, and Vladimir Kramnik. “By learning near-optimal strategies for each variant with AlphaZero, we determine what games between strong human players might look like if these variants were adopted.”

A Grand Unified Theory of the AI Hype Cycle, by Glyph.

Iconv, set the charset to RCE: Exploiting the glibc to hack the PHP engine (part 1), by Charles Fol. Kill it with fire, I’d say.

Taming Floating-Point Sums in Rust, by Orson R. L. Peters.

Schröders Traum, “Bruno Schröder war Bergmann in Ibbenbüren. Als er stirbt, hinterlässt er 70.000 Bücher.”

City In A Bottle – A 256 Byte Raycasting System

The world’s last internet cafes

Quine Clock

NASA’s Voyager 1 Resumes Sending Engineering Updates to Earth

Lix is a modern, delicious implementation of the Nix package manager, focused on correctness, usability, and growth – and committed to doing right by its community.

New Foundations is consistent, a digitisation of Randall Holmes’ proof in Lean 4.

Periodic orbits for Newtonian planar three-body problem, by Xiaoming LI and Shijun LIAO.

Drawing hat tiling using Racket

Pytype checks and infers types for your Python code—without requiring type annotations.

Inclusive Sans is a text font designed for accessibility and readability.

MS-DOS v4.0, now MIT-licensed.

LGBTeX, a logo by Alessandra Sierra.

Bible errata

Building a GPS Receiver using RTL-SDR, by Phillip Tennen.

Reproducing EGA typesetting with LaTeX, using the Baskervaldx font.

The Solution of the Zodiac Killer’s 340-Character Cipher, final, comprehensive report on the project by David Oranchak, Sam Blake, and Jarl Van Eycke.

Bridging brains: exploring neurosexism and gendered stereotypes in a mindsport, by Samantha Punch, Miriam Snellgrove, Elizabeth Graham, Charlotte McPherson, and Jessica Cleary.

Yotta is a minimalistic forth-like language bootstrapped from x86_64 machine code.

SSSL - Hackless SSL bypass for the Wii U, released one day after shutdown of the official Nintendo servers.

stagex, a container-native, full-source bootstrapped, and reproducible toolchain.

Computing Adler32 Checksums at 41 GB/s, by wooosh.

Random musings on the Agile Manifesto

doom-htop, “Ever wondered whether htop could be used to render the graphics of cult video games?”

A proper cup of tea, try this game!