## Posts

### What if undecidability shows up all at once?

### www.thug.com

### Pro-AI?

### `eval` should not be a built-in function

### Tetration

### Python Interface / Refactor Challenge

### Blogging in the Age of Internet-Scale AI Training

### When Only Real Math Will Do

### The High Price of Abstraction in Python

### There is no such thing as human-generated text

### How to Print-Debug Python Comprehensions

### Some Advice for Browsing Wiktionary in Emacs

### The Walrus-While Python Pattern

### Collatz Counterexamples

### How Typical is the Solar System?

### Formal Proof Challenge: The Half-Collatz Theorem

### Heaven Must Be Missing a Syllable

### A Solution to the Halting Problem

### Does This Function Terminate?

### Performance Hot Spots

### Collatz Arithmetic

### Total Functions and Partial Functions

### A Formal Theory of Spaghetti Code

### ذس پوست س رتن ن ینگلش

### Latest Beeping Busy Beaver Results

### Brady's Algorithm for Program Generation

### Another New Record in Self-Cleaning Turing Machines

### A Better Turing Machine Tape Model

### A History of Busy Beaver Hardware

### Binary Relations in Idris

### A Busy Beaver Champion Program Derived from Scratch

### Maybe the Spaghetti Code Conjecture is False

### Exciting New Ways To Be Told That Your Python Code is Bad

### A New Record in Self-Cleaning Turing Machines

### Structured Programming for Busy Beavers

### An Ounce of Riot Prevention is Worth a Pound of Riot Cure

### A Mathematical Fact from a Busy Beaver

### signed char lotte

### Lin Recurrence and Lin's Algorithm

### Blanking Beavers

### The Spaghetti Code Conjecture

### Halt, Quasihalt, Recur

### The Lin-Rado Busy Beaver Proof

### A Christmas Tautology

### Is the Busy Beaver Sequence Well-Defined?

### Beeping Busy Beaver Results

### The Afterlife Behavior of Quasihalting Turing Machines

### Turing Machine Notation and Normal Form

### Are Turing Machines Programmable?

### Beeping Busy Beavers

### A Makefile for Getting Dressed

### Derek Chauvin Did This

### The Pronunciation of 'Kernighan', according to Foreign-Language Wikipedia

### Idris Algebra

### Why Aren't Idris Interfaces Verified?

### Answers to Questions about Chinese Characters and Dictionaries

### A Partly-Successful Attempt to Look Up a Chinese Character

### Dependently-Typed Proofs are Code, and Repetitive Code is Bad, So...

### The Disco Fallacy

### Material Implication is Not Paradoxical

### Modified Emacs Mac Modifiers

### Four Years of Twenty-Five Days of Christmas Movies

### Emacs Lisp Challenge: flaky-if

### Book Review: The Little Typer

### A Correctness Proof for a Simple Compiler in Idris

### Python's `RecursionError` is a Misnomer

### Recursion Error While Handling Recursion Error

### I Got a Knuth Check for 0x$3.00

### Lispier Rust with Generics

### Remacs FAQ

### Propositional Logic Theorems as Types in Idris

### The Magic SysRq Key

### The Story of XEmacs

### Some Advice for How to Make Emacs Tetris Harder

### My First Emacs Commit

### Real-World Uses for Dynamic Scope

### The Bubble Sort Machine

### Basic Web Scraping with Emacs

### Grepping Dictionaries, English and Otherwise

### Who Wrote the One-Star Reviews of SICP?

### Logic in Reazon II: Generating Propositional Logic Proofs

### Logic in Reazon I: Generating Sentences of Modal Logic

### Proving the Second Incompleteness Theorem from the First

### Solving Logic Puzzles in Emacs with Reazon

### The Python `in` Keyword(s)

### Anonymous Recursive Functions

subscribe via RSS