research!rsc: Pulling a New Proof from Knuth’s Fixed-Point Printer

Russ Cox presents an alternative proof of correctness for Donald Knuth's P2 algorithm, which converts 16-bit fixed-point binary fractions to shortest accurate decimal representations. Starting with a trivially correct program in Ivy (an APL-like calculator language), Cox incrementally transforms it into Knuth's P2 through a series of proven steps: walking digits until endpoints diverge, premultiplication optimization, collecting digits iteratively, change of basis, and scaling to eliminate rationals. The post also explores simpler alternative solutions including a Schubfach-inspired approach and rediscovers a textbook solution from Knuth's own Volume 2 (based on Taranto's algorithm, extended by Steele and White). Cox argues this incremental proof approach is more comprehensible than Knuth's original proof, demonstrating how programming language capabilities shape both programs and their proofs.