Hillel Wayne

Key Insight: Predicate logic gives programmers a precise, unambiguous tool for specifying system requirements, and the central tension across all logical systems is the ability-guarantee tradeoff: expressive power always comes at the cost of provable properties.

This post is an adapted chapter from Hillel Wayne's book 'Logic for Programmers,' offering a ground-up introduction to predicate logic using programming-familiar examples. Wayne defines predicates as abstract Boolean functions that can express things beyond computation, then builds up the implication operator, sets, and quantifiers (some/all) through concrete scenarios like system requirements and pull request workflows. A central thread is that formalizing requirements in logic exposes ambiguities invisible in natural language. The chapter culminates in rewrite rules and a unifying principle: the ability-guarantee tradeoff, where more expressive systems offer greater power but fewer provable properties. The notation throughout is deliberately keyboard-typeable, prioritizing accessibility over mathematical convention.

Key Insight: Formal logic is foundational to understanding software, yet programmers have been left to acquire it through osmosis by default — a gap this book directly addresses with a rigorous but math-free curriculum.

Hillel Wayne announces the 1.0 release of his book 'Logic for Programmers,' five years in the making. His central argument is that formal logic is a surprisingly powerful tool for understanding everyday software concepts, yet no programmer-focused resource for learning it existed. Developers were expected to either read dense math textbooks or absorb it through osmosis — and the osmosis route doesn't work. The book targets working developers with zero math background, covering logic basics and applications ranging from property-based testing to domain modeling to logic programming. Each chapter was reviewed by both a domain expert and a junior programmer to ensure accuracy and accessibility.

Key Insight: Comparing Chicago deep dish to New York pizza is a category error — they serve entirely different culinary roles, and the real comparison should be between everyday iconic foods from each city.

In this April Cools post, Hillel Wayne argues that the classic 'Chicago vs New York pizza' debate is fundamentally flawed because deep dish and New York pizza serve completely different culinary roles. Deep dish is a special occasion food that Chicagoans rarely eat, while New York pizza is everyday lunch fare. The proper comparison, he argues, is New York pizza versus the Chicago hot dog, which serves the same everyday-lunch role. After comparing the two, he reluctantly gives the edge to New York pizza for home-cooking convenience, but uses the post mainly as an excuse to celebrate underappreciated Chicago foods like Italian beef and flaming saganaki.

Key Insight: Z3 is a remarkably versatile tool that can solve equations, prove theorems, and reverse engineer algorithms, but choosing good pedagogical examples requires balancing accessibility, practicality, and tool-appropriateness.

Hillel Wayne shares a collection of Z3 SMT solver examples that were cut from his book Logic for Programmers. He walks through increasingly complex uses: solving systems of equations, proving no four distinct positive integers share both sum and product, optimizing financial contributions, reverse engineering RNG parameters, proving mathematical theorems, and modeling stock trading with Z3 arrays. He explains why most examples didn't make the book's final cut—they either weren't practical enough, required too much background explanation, or weren't the right tool for the job—and describes the three examples he ultimately chose.

Key Insight: The algebraic properties that give algebraic data types their name—associativity, distributivity, cardinality relationships—were all present in McCarthy's foundational 1961 paper, decades before the terminology was standardized.

This post traces the origins of algebraic data types (AlgDTs) from John McCarthy's 1961 paper through their development in both imperative and functional programming traditions. McCarthy first defined the concepts of Cartesian products and direct unions (sum types) along with their algebraic properties like distributivity and associativity. The ideas influenced Tony Hoare and Rod Burstall, who developed them independently in different directions. While sum types disappeared from imperative languages due to Pascal and C's influence, they flourished in functional programming through ML, HOPE, and Miranda, eventually gaining features like tags, exhaustiveness checking, and pattern matching that define modern AlgDTs.

Key Insight: Gaming's accessibility problem isn't about complexity—Stardew Valley is more intricate than many 'complicated' games—but about whether the complexity is introduced in an approachable way that doesn't assume prior gaming literacy.

Hillel Wayne offers a guide to video games for non-gamers, noting that despite gaming being a $500 billion industry, many people have never played because games assume existing 'vocabulary' of conventions. He proposes four criteria for good introductory games: no special hardware required, no assumed gaming knowledge, cultural significance, and personal verification that non-gamers enjoyed them. He then recommends four games—Baba is You (puzzle), Stardew Valley (farming sim), The Case of the Golden Idol (deduction), and Balatro (roguelike)—explaining each game's mechanics, appeal, and place in gaming history.

Key Insight: JavaScript's bizarre --> comment syntax exists because the web's commitment to backward compatibility means even temporary hacks from 1995 get standardized forever.

This post presents a JavaScript parsing puzzle where the expression 'x = 1' followed by 'x' and '--> 0' unexpectedly prints 1. The trick is that '-->' at the beginning of a line is a valid comment token in JavaScript, a legacy feature preserved from the days when developers wrapped scripts in HTML comments to hide them from older browsers that didn't understand the script tag. This hack was standardized in ECMAScript 2015 to avoid breaking old websites, demonstrating how backward compatibility concerns shape language design.

Key Insight: Software's constructed interfaces make engineering controls unusually cost-effective compared to physical systems, so we should bias toward building safety into systems rather than relying on training and procedures.

Hillel Wayne adapts the Hierarchy of Controls (HoC) from workplace safety to software engineering, using his own experience of accidentally dropping a production database as a case study. The hierarchy ranks controls from most to least effective: elimination, substitution, engineering controls, administrative controls, and PPE. He argues that software is particularly well-suited for engineering controls since all interfaces are constructed rather than natural, making it easier to build in safeguards. The post notes that controls can themselves introduce new hazards and should be considered holistically. PPE translates poorly to software contexts since the framework was designed to protect humans from machines, not machines from humans.

Key Insight: Sometimes you have to pause one project to focus on completing another.

Hillel Wayne announces a temporary pause in blog writing to focus on completing his book 'Logic for Programmers'. He expects to resume blogging in early 2025. He notes that his weekly newsletter will continue during this hiatus.

Key Insight: The best programming languages for quick problem-solving aren't necessarily the best general-purpose languages - specialized 'toolbox' languages that prioritize terseness and rich builtins can dramatically outperform Python for specific domains.

Hillel Wayne introduces the concept of 'toolbox languages' - programming languages optimized for quickly solving problems without third-party dependencies. He showcases five personal favorites beyond Python: AutoHotKey for GUI automation, J for terse array computations, Frink for dimensional analysis with units, Raku for scripting with powerful syntactic features, and Picat for logic programming with constraint solving. The post argues that good toolbox languages prioritize speed of writing over other concerns, with terseness, rich builtins, and good REPLs being key characteristics.

Key Insight: By leveraging TLA+'s dual interpretation of primed variables as both assignments and constraints, you can compose large specifications through a central Sync operator that guards and triggers transitions without modifying the original components.

This post presents a technique for composing large TLA+ specifications using state machines and a 'Sync' operator. The traditional approach to composing specs requires manually stitching together actions, which becomes unwieldy for large specifications. Wayne's solution uses TLA+'s ability to treat primed variables as both assignments and constraints, allowing a central state machine to guard and trigger transitions across independent components. The technique involves writing an abstract state machine for the core component, keeping other components 'open' (not fully self-contained), and using refinement to verify correctness. While more complex than simple specs warrant, this approach scales better for large specifications that need independent development.

Key Insight: Software development friction—the accumulated gap between theoretical simplicity and practical difficulty—is inevitable, compounds non-linearly, and fighting it can create new friction.

Hillel Wayne applies Clausewitz's military concept of 'friction' to software development, arguing that the gap between theoretical simplicity and practical difficulty is a fundamental, unavoidable aspect of building software. He catalogs diverse sources of friction—from API changes and bugs to sick kids and stolen laptops—and notes that friction compounds: two setbacks are more than twice as bad as one. The post explores how friction accumulates over time and scope, and how attempts to address it can create new friction. Wayne concludes with open questions about categorizing friction, learning from other fields, and whether individual awareness of friction provides value.

Key Insight: In formal specification, making illegal states unrepresentable through facts prevents you from verifying that your software correctly handles those illegal states when they occur in the real world.

The post warns against overusing Alloy's 'fact' keyword to constrain specification models. While facts prevent the model checker from generating certain states, this can backfire when you need to verify that your software correctly handles invalid inputs. The author argues that 'making illegal states unrepresentable' works well in programming but creates problems in specification because specs must model both the software and its environment. Using predicates instead of facts keeps constraints explicit and testable. Facts should be reserved for narrowing problem scope, eliminating uninteresting cases, optimization, or expressing relationships Alloy can't handle natively.

Key Insight: The modern name Daniel may represent an unbroken 3,400-year chain of cultural transmission, surviving the Bronze Age Collapse through shared Canaanite religious traditions and later preserved by the name's theological importance in Christianity.

Hillel Wayne traces the etymology of the name 'Daniel' from its earliest known written appearance in Ugaritic texts from approximately 1350 BCE to its modern ubiquity. Starting from clay tablets discovered in the ruins of Ugarit, he follows the name through the Bronze Age Collapse, the Phoenician era, and into the Hebrew Bible. The investigation reveals that while the exact pronunciation may have shifted (from 'Danel' to 'Daniel'), the meaning 'judged by El/God' has remained consistent across 3,400 years. The name's survival into modernity is largely attributed to the Book of Daniel's importance in Christian theology, which kept it in mainstream use across cultures worldwide.

Key Insight: The absence of graph types in programming languages isn't an oversight but a consequence of the impossibly large design space combined with performance requirements so stringent that generic abstractions consistently fail real-world use cases.

The post investigates why graphs, despite being ubiquitous in software (package dependencies, databases, state spaces, social networks), lack native support in mainstream programming languages. Through interviews with graph algorithm experts, library maintainers, and database engineers, Wayne identifies three interconnected reasons: the overwhelming number of graph type variations (directed, undirected, multigraphs, hypergraphs), the many possible internal representations (edge lists, adjacency matrices, etc.) each with different performance tradeoffs, and the critical importance of performance optimization for graph algorithms that are often NP-complete and run on enormous datasets. The conclusion is that the design space is simply too large and performance-sensitive for standard libraries to provide useful abstractions.

Key Insight: Planning as a programming paradigm—finding sequences of state mutations to reach goals—offers an elegant middle ground between imperative programming and constraint solving that makes certain hard problems surprisingly tractable.

Hillel Wayne introduces Picat's planner module, which extends logic programming by finding variable mutations that reach desired end states rather than just finding satisfying assignments. He demonstrates this through a grid pathfinding problem, progressively adding complexity: first basic movement, then multiple ordered goals, then optimal path finding across unordered goals. The planner elegantly handles each extension with minimal code changes, and can even combine with constraint solving for problems like finding the largest partitionable subset of numbers. Wayne concludes that while Picat isn't production-ready due to poor documentation and error messages, it excels as a toolkit language for specific computational problems.

Key Insight: A simple mental arithmetic trick for generating random digits is actually a multiply-with-carry RNG in disguise, and understanding the underlying math reveals which multipliers produce the best randomness.

Hillel Wayne explores a mental random number generator algorithm originally posted by George Marsaglia on Usenet. The technique involves starting with a 2-digit seed, then repeatedly computing a new number by adding the tens digit to 6 times the units digit. Wayne investigates why this works using Raku, discovering that only certain multipliers (like 6, 11, 18) produce a single orbit covering all values. He explains the connection to multiply-with-carry and Lehmer RNGs, ultimately recommending 18 as a multiplier for better randomness despite requiring memorization of the 18 times-table.

Key Insight: When designing systems, you must faithfully model the world you can't control while only implementing the machine you can—and observable properties that affect users matter far more than internal implementation details.

This post introduces a conceptual framework from Michael Jackson for thinking about formal specifications: the distinction between 'machine' (the part of the system you control) and 'world' (everything you don't). Using a TLA+ bank transfer example with a race condition bug, Hillel demonstrates that solutions must work within the machine's boundaries—you can add a lock to serialize transactions, but you can't control how people use their checkbooks. The post elaborates on observability (which states each domain can read/write) and distinguishes between internal properties (implementation details) and observable properties (what users actually experience). The key insight is that observable properties matter more because they're what actually affects people.

Key Insight: Great conferences, like great software, reflect a singular vision that cannot be replicated—only honored through something fundamentally different.

This post collects Hillel Wayne's impressions of talks he attended at the final Strangeloop 2023 conference. He covers topics ranging from career advice and play in engineering to LLMs, stack-based languages, comedy with generative models, permacomputing sustainability, formal methods accessibility, and teaching difficult concepts. The post concludes with a personal reflection on how Strangeloop shaped his career and the unique community it fostered. Wayne notes that while a successor conference might emerge, it cannot replicate what made Strangeloop special—it was fundamentally Alex Miller's vision.

Key Insight: The Liskov Substitution Principle becomes intuitive when reframed as a testing concept: a subtype must pass all black-box tests written for its parent type.

Hillel Wayne presents a more intuitive way to understand the Liskov Substitution Principle: if a class inherits from another, it should pass all of the parent's black-box tests. The traditional approach uses three rules (method contracts, class invariants, and the history rule), but these feel arbitrary and disconnected. The testing approach unifies all three rules under one simple concept. Research by Baniassad and Summers found this pedagogical reframing significantly improved student understanding of LSP, taking them from failing to passing grades on related questions.

Key Insight: Refinement offers a mathematically rigorous bridge between abstract design and concrete implementation, but the exponential cost of verifying detailed specs makes it too burdensome for most real-world engineering — making it an elegant idea that rarely escapes academia.

Hillel Wayne explains specification refinement in TLA+ as a technique for connecting formal specifications to concrete implementations. Refinement is formally defined as ImplSpec => AbstractSpec: any behavior of the implementation must also be a valid behavior of the abstract design. Using a multithreaded counter as a running example, Wayne demonstrates how a naive non-atomic implementation fails refinement — exposing a race condition — while a lock-based implementation succeeds. He explains what guarantees refinement provides (safety and liveness properties flow downward from abstract to concrete) and surveys the serious practical challenges that limit industrial adoption. He concludes that while spec-to-spec refinement has niche value, spec-to-code refinement is unlikely to see broad use.

Key Insight: When code lacks inferable outputs or mathematical properties, the existing production version is the best correctness oracle available — and property testing against it via git worktree can catch subtle refactoring bugs that no other technique would find.

Wayne introduces 'rho problems' — a class of code that's hard to test because outputs aren't inferable from inputs, lack mathematical properties, and can contain subtle bugs affecting only a small fraction of inputs. Examples include computer vision, simulations, and data pipelines. He proposes 'cross-branch testing': using the production/deploy branch itself as a correctness oracle, combined with property-based testing to generate random inputs. Using `git worktree`, both the deploy branch and the refactor branch can be loaded simultaneously, and a property test simply asserts their outputs always agree. The technique caught a subtle 1% bug in his contrived example that unit tests and traditional property tests would miss.

Key Insight: The blanket advice to avoid 'clever code' conflates harmful language-trick cleverness with valuable problem-insight cleverness, and recognizing this distinction is essential for honest discussions about tools, languages, and expertise.

Hillel Wayne distinguishes between two kinds of 'clever code': language-trick cleverness (like Duff's Device) and problem-insight cleverness (like using bucket sort when you know the data range). He argues that while the first kind deserves its bad reputation, insightful code can be faster, simpler, and safer than naive alternatives. However, insight is fragile—it depends on specific problem properties that may change—and non-transferable between team members. Wayne shows how insight acts as a confounding factor in language benchmarks and as an adoption barrier for tools like property-based testing and formal specification languages, ultimately calling for more nuanced discussions about cleverness in software engineering.

Key Insight: Specifications resist modular composition because each spec must totally describe the behavior of all its variables, and combining specs that share state inevitably produces contradictory requirements that can only be resolved by manually examining and integrating their internals.

The post explores why formal specifications don't compose well, walking through increasingly complex attempts to combine two simple 'blinker' specs in Linear Temporal Logic. Starting with naive conjunction, each attempt reveals a new obstacle: synchronization constraints, the frame problem, fairness violations, and stuttering requirements. Even after making specs stutter-invariant to recover some composability, introducing shared state between specs causes deadlock-like failures. The conclusion is that specs must totally describe how their variables change, and component specs don't know about each other's variables, forcing practitioners to manually stitch specs together rather than compose them modularly.

Key Insight: Linked list interview questions began as practical tests for C programming experience in the 1980s, but lost their original context and became cargo-culted as 'CS fundamentals' tests despite being irrelevant to most modern programming work.

Hillel Wayne investigates why tech companies ask linked list questions in interviews, using historical research methods to trace their origins. Through interviewing older programmers, analyzing 1980s Usenet archives, and examining job postings, he builds evidence that these questions originated as practical tests for C and Pascal experience—languages that required manual pointer manipulation. The practice persisted and spread through influential figures like Joel Spolsky and Gayle Laakmann McDowell, who exported questions from low-level companies like Microsoft and Google. Ironically, the original context was lost, and people now justify these questions with post-hoc rationalizations about 'CS fundamentals' or 'quick thinking.'

Key Insight: Action properties fill the gap between state invariants and liveness properties by validating transitions—catching invalid changes between states that are individually acceptable.

This post explains TLA+ action properties, which are properties that apply to state transitions rather than individual states. Unlike invariants that must hold for every state, action properties validate pairs of states—ensuring transitions are valid even when both states are individually acceptable. The post provides the syntax `[][A]_x` for expressing these properties while respecting TLA+'s stutter invariance. Wayne positions this as 'intermediate-level' content filling a gap between introductions and case studies, offering practical patterns for conditional properties, state machines, and various real-world constraints.

Key Insight: Software and traditional engineering have each optimized for different aspects of the craft—we should adopt each other's strengths rather than assuming inherent tradeoffs prevent it.

This essay concludes Wayne's 'Crossover Project' exploring what software engineers can learn from traditional engineers and vice versa. Through interviews with engineers who crossed between fields, Wayne finds that traditional engineers excel at planning, requirements gathering, and professional responsibility, while software engineers have developed superior open communities and revolutionary version control systems. The key insight is that these differences aren't essential tradeoffs—both disciplines could adopt each other's strengths. Wayne argues software engineers should spend more time thinking before coding, while traditional engineering could benefit enormously from our collaborative culture and tools like git.

Key Insight: Software engineering's supposed uniqueness is largely a self-serving myth; we share the same fundamental challenges as all engineering disciplines, and recognizing this opens opportunities for cross-disciplinary learning.

Hillel Wayne argues that software engineering is not fundamentally different from traditional engineering disciplines, despite common beliefs. Through interviews with crossover engineers (people who worked in both software and traditional engineering), he systematically dismantles claims that software uniquely requires Agile, is more unpredictable, or is less rigorous. While acknowledging real differences—software's consistency, faster iteration velocity, and softer constraints—he concludes these don't make software 'special' but rather just another engineering discipline with its own challenges, similar to how chemical and civil engineering each have unique concerns.

Key Insight: The debate over whether software engineering is 'real' engineering has been conducted entirely by people who've never worked as traditional engineers; those who have crossed over from traditional engineering mostly say yes, it counts.

Hillel Wayne investigates whether software engineering deserves to be called 'engineering' by interviewing 17 professionals who worked as traditional engineers before becoming software developers. He systematically dismantles common arguments against the title—that software lacks math, high consequences, or licensing—showing that these don't define engineering in other fields either. Of the crossovers interviewed, 15 considered software engineering to be real engineering. Wayne concludes that while not all software developers are engineers, the gap between software development and software engineering is much smaller than in traditional fields, separated by circumstance rather than essence.

Key Insight: What appears to be deliberate design is often inherited convention, and understanding the deeper historical layers reveals the actual constraints and forces that shaped our tools.

Hillel Wayne explores two computing history puzzles—why Vim uses hjkl for navigation and why JavaScript months are 0-indexed—to illustrate how historical explanations have layers. The surface answers (home row efficiency, array indexing convenience) are post-hoc rationalizations. Digging deeper reveals that hjkl was inherited from the ADM-3A terminal's control key conventions rooted in ASCII bit manipulation, while 0-indexed months came from early Unix memory optimization on the PDP-7. Wayne argues that understanding these deeper layers reveals the actual forces that shaped our tools, though each layer requires exponentially more research effort to uncover.

Key Insight: Adding workers to a task queue doesn't just improve throughput linearly—it fundamentally changes the mathematical behavior of latency from quadratic to sublinear growth.

This post demonstrates how to use PRISM, a probabilistic model checker, to analyze task queue performance. The author builds progressively complex models showing that while throughput scales linearly with workers (2x workers ≈ 2x throughput), latency behaves counterintuitively—growing quadratically with task volume for a single worker. Adding a second worker doesn't just halve latency; it fundamentally changes the growth pattern from quadratic to sublinear because queue jams require both workers to stall simultaneously. The post walks through the PRISM specification language, explains how to model both throughput and latency using reward functions, and concludes by generalizing the model using binomial expansion to handle arbitrary numbers of workers.

Key Insight: The adoption gap for software correctness tools is primarily a usability problem, not a developer apathy problem, and it's within our power to fix.

Wayne argues that the reason programmers don't adopt software correctness techniques isn't laziness or apathy, but inconvenience. He draws an analogy to flossing: everyone knows root canals are worse than buggy software, yet most people don't floss daily because it's fiddly and annoying. The same dynamic applies to TDD, type systems, and formal methods. He points to Ruby's rspec ecosystem and Elm/TypeScript's user-friendly tooling as evidence that convenience drives adoption. Wayne concludes that communities wanting mainstream adoption should focus on improving UI/UX, documentation, and tooling rather than blaming outsiders for not caring about correctness.

Key Insight: Formal specification with TLA+ can catch subtle concurrency bugs like deadlocks before they reach production, and the effort to write specs is comparable to writing the original code while being reusable across similar problems.

This post demonstrates how to use TLA+ to model and verify a Go concurrency bug originally described by Chris Siebenmann. The author walks through translating Go code with goroutines, channels, and defer statements into a PlusCal specification, showing how to model both buffered and unbuffered channels. The TLA+ model checker successfully reproduces the deadlock and verifies that three proposed fixes all work correctly. The post concludes by noting that while TLA+ works for this purpose, Spin might be better suited for Go channel semantics since it has channels as a native datatype.

Key Insight: Decision tables are low-cost formal specifications that help catch design errors by forcing explicit enumeration of all input-output mappings, but their simplicity means they're best suited for discrete, independent inputs rather than complex state or temporal logic.

This post provides a comprehensive guide to decision tables, a specification tool that maps finite enumerated inputs to outputs. Wayne explains that decision tables must be complete (covering all input combinations) and sound (no conflicting outputs) to be valid, making them a form of formal specification. He distinguishes decision tables from pattern matching by emphasizing they work at any abstraction level for design, not just code. The bulk of the post covers techniques to manage table bloat, including wildcards, decomposition, and handling dependent inputs and intervals. Wayne concludes by identifying when decision tables become inappropriate—complex data structures, time-based decisions, or when formalism doesn't add clarity.

Key Insight: APL's power comes not from its notorious syntax but from treating arrays as primitives and making transformations like filtering and sorting into first-class, manipulable data structures.

This post explores how J (a successor to APL) embodies Kenneth Iverson's idea that better notation leads to deeper mathematical insights. Rather than focusing on APL's infamous terse syntax, the author demonstrates how treating arrays as primitives—rather than collections of scalars—fundamentally changes how we think about programming. Through examples of rank manipulation, sieves for filtering, and grades for sorting, the post shows that APL's essence lies in its conceptual model of array transformations, not its cryptic symbols. The author argues that learning J made them a better programmer by teaching them to think about operations on entire arrays at once.

Key Insight: Cheatsheets optimized for experts fail learners because density helps only those who already know what they're looking for - progressive revelation matches the reference material to the student's evolving mental model.

Hillel Wayne presents a practical improvement to traditional cheatsheets for teaching formal methods workshops. He identifies that standard dense cheatsheets overwhelm students who don't yet have mental models to navigate them, leading to two failure modes: using wrong concepts or being unable to locate relevant information. His solution is 'progressive cheatsheets' where students receive increasingly complete versions as they progress through the material. A key refinement ensures layout consistency across all versions by rendering hidden content as white text rather than removing it, preventing students from having to relearn content locations.

Key Insight: Unit handling in software is a deceptively complex problem that most languages ignore, but Frink demonstrates that a purpose-built language can make dimensional analysis both rigorous and pleasant to use interactively.

The post introduces Frink, a programming language designed specifically for handling units of measurement with dimensional analysis. Wayne explains why units are surprisingly complex—different measurement systems, historical variations, ambiguous dimensions, and uncertainties all create challenges that most programming languages handle poorly. Frink strikes a balance between the strict compile-time checking of F# and the simple conversion tool GNU units, offering runtime flexibility with built-in dimensional analysis. The language includes over 5,000 predefined units, natural mathematical syntax, and affordances like interval arithmetic and timestamp handling. Wayne demonstrates its practical value by calculating the calories in homemade chocolates, showing how Frink handles mixed units and uncertainty naturally.

Key Insight: The distinction between weak and strong fairness determines whether a concurrent system must guarantee progress for actions that are permanently enabled versus those that are only intermittently enabled, with real-world systems often choosing weaker guarantees for practical reasons.

This post explains the distinction between weak and strong fairness in TLA+ specifications, concepts that determine whether concurrent systems are guaranteed to make progress. Fairness addresses whether actions that can happen will eventually happen, preventing specifications from allowing infinite 'stuttering' where systems freeze. Weak fairness guarantees an action happens if it's permanently enabled, while strong fairness guarantees it happens if it's intermittently enabled. The post uses clock and worker retry examples to illustrate how unfair, weakly fair, and strongly fair systems behave differently. Wayne notes that even production systems like Microsoft's thread scheduler opt for weak rather than strong fairness for practical tradeoffs.

Key Insight: Generating valid test inputs by construction through composite strategies is more effective than filtering invalid random inputs, and is essential for testing code with interdependent data structures.

This tutorial addresses one of the two hard parts of property-based testing: generating complex, interdependent inputs. Using an exam/exam-instance example, it walks through Hypothesis strategies from simple (type inference, filter, assume) to sophisticated (builds, composite, data). The key challenge is generating data with preconditions and dependencies—like ensuring an ExamInstance's answers match its Exam's length. Composite strategies emerge as the most powerful tool, allowing multiple draws to be related to each other. The tutorial emphasizes that generating valid inputs by construction is better than filtering invalid ones.

Key Insight: Making illegal states unrepresentable is not universally superior—it's a tradeoff that works well for monotonic properties but struggles with negation, overlapping categories, and the need to represent undesirable-but-valid states.

The post explores two approaches to data validation: predicative (using boolean functions to filter valid items from all representable states) and constructive (structuring data so only valid states can be created). While the constructive approach of 'making illegal states unrepresentable' is often seen as obviously superior, Wayne argues it has significant limitations including ergonomic costs, difficulty handling overlapping categories, and poor support for nonmonotonic properties. He concludes that most real-world data will be a mix of both approaches, and that finding good constructive solutions is a learnable skill with identifiable patterns.

Key Insight: The friction of customization matters more than the possibility of customization - when adding small workflow improvements is easy, you actually do it; when it requires deep technical knowledge, you don't.

Hillel Wayne explains why he prefers Windows over other operating systems despite its shortcomings: AutoHotKey makes customization trivially easy. He walks through progressively complex scripts he's written, from simple mouse button remapping to automated sci-hub paper retrieval. The key insight is that while similar functionality might be achievable on Mac or Linux, the friction of implementation matters enormously. When adding affordances is easy, you actually add them; when it requires diving into OS internals, you don't bother.

Key Insight: The hard part of learning a new language isn't the language itself—it's the hundred practical questions about tooling, ecosystem, and workflow that no tutorial ever answers.

Wayne captures the frustrating experience of trying to adopt a new programming language despite theoretical advantages. While online tutorials make languages look appealing, the practical obstacles of tooling, documentation, debugging, and ecosystem are overwhelming. The accumulating friction of answering dozens of mundane questions—none addressed by tutorials—drives developers back to familiar languages. The post is a compact catalog of the real barriers to language adoption that have nothing to do with syntax or semantics.

Key Insight: Technical tools often fail to gain adoption not because of their complexity, but because of accessibility barriers like requiring paid resources to learn them.

Hillel Wayne announces the first draft of an online Alloy reference documentation hosted on ReadTheDocs. He argues that Alloy's biggest adoption barrier isn't technical but social—requiring people to buy a book to learn it. The documentation covers language syntax, tooling, techniques for better specs, and troubleshooting. While still incomplete and unofficial, Wayne believes it will help people learn Alloy and welcomes community feedback via GitHub.

Key Insight: The most influential programming languages in history are often not the most popular ones, but forgotten research languages whose ideas were absorbed by their successors—making the study of 'dead' languages essential for understanding modern computing.

This post surveys ten historically significant programming languages that are now mostly forgotten or dead, arguing that their influence on modern computing far exceeds their current recognition. Wayne methodically traces how features we take for granted—from structured data to OOP to type inference—originated in languages like COBOL, ALGOL, SIMULA, and CLU. He emphasizes that determining true influence requires citation chains, not just temporal precedence, since independent invention is common. The post serves as both a history lesson and a critique of lists that focus only on currently popular languages while ignoring the foundational work that made them possible.

Key Insight: Science functions as a social institution where markers of trust and integrity serve as necessary heuristics, making replication and open data essential not just for accuracy but for the credibility that allows valid critiques to be heard.

Hillel Wayne traces the dramatic saga of a 2014 academic paper claiming to link programming language choice to code defect rates through GitHub mining. The original FSE paper made significant methodological errors, including misclassifying C++ projects as TypeScript and counting duplicate commits from Bitcoin forks. A 2019 replication study exposed these flaws, finding that one-third of 'defect-fixing commits' weren't actually bug fixes. The ensuing academic feud, complete with rebuttals and counter-rebuttals, reveals how science functions as a social institution where trust, integrity, and reputation matter as much as data. Wayne ultimately sides with the replicators after discovering the original authors failed to properly read a spreadsheet that refuted their own rebuttal.

Key Insight: Feature interaction bugs emerge when individually correct features combine to violate global properties, making them invisible to unit tests and requiring formal specification or domain expert involvement to detect.

Feature interaction bugs occur when individually correct features combine to break global system properties. Wayne demonstrates this through a detailed example of an email registration system where spam blocking, email changing, and verification resending features each work correctly in isolation but combine to allow spammers through. These bugs are especially insidious because they don't map to isolated components and can't be caught by unit tests. While formal specification tools like TLA+ and Alloy can detect these issues, ultimately addressing feature interaction requires involving domain experts, maintaining constant communication, and continuously evaluating how local changes affect the big picture.

Key Insight: Formal methods pay for themselves by finding subtle, expensive bugs at the design stage—before you've spent weeks building the wrong system.

Hillel Wayne presents a practical business case for formal methods, arguing that specification-based design verification saves money by catching complex bugs before implementation. He demonstrates using a carbon credit trading platform example where a subtle race condition—taking three actors and four steps to manifest—would slip past unit tests and QA. A 50-line TLA+ specification finds this bug in under six minutes total effort. He also honestly addresses limitations: no automatic code generation, less useful for simple systems, and poor at catching implementation errors like null handling.

Key Insight: Understanding hyperproperties—properties over sets of behaviors rather than individual traces—explains why security is hard, why tests catch things types miss, and provides a powerful lens for thinking about system correctness.

Hyperproperties are properties defined over sets of behaviors rather than individual traces, making them fundamentally different from traditional safety and liveness properties. While TLA+ cannot natively express hyperproperties, you can work around this limitation through 'self-composition'—creating a hyperspec that runs multiple copies of the original spec and compares their results. The post walks through a concrete example of checking Observational Determinism (whether a nondeterministic system appears deterministic to outside observers) using this technique. Most hyperproperty research focuses on security properties like noninterference, though the formalism has seen limited industrial adoption. Wayne argues that understanding hyperproperties provides valuable intuition for verification, explaining why tests are better at capturing relationships between function calls than types or contracts.

Key Insight: Automated transcription, even when inaccurate, provides sufficient data for self-analysis, and deliberate practice with measurable targets can materially improve professional skills like public speaking.

Hillel Wayne investigates his speaking pace at conference talks, which he knows is too fast. He uses AWS transcription to analyze two of his talks, discovering he speaks at about 194 words per minute—significantly faster than Obama's 120 wpm baseline. Through practice with specific pacing exercises and a custom vim configuration to estimate talk lengths, he successfully reduced his pace to 163 wpm for a subsequent talk while covering the same amount of content, proving that slowing down doesn't sacrifice information density.

Key Insight: Formal methods aren't just for distributed systems—they're equally valuable for verifying database migrations by proving that data transformations preserve both equivalence and validity constraints.

The post demonstrates how to use Alloy, a formal specification language, to model and verify database migrations. Wayne walks through specifying an old schema (Person with event relationships) and a new schema (separate Attendance and Review tables), then proves that migrations preserve data equivalence and validity constraints. The tutorial reveals subtle bugs in the migration spec—like accidentally allowing extra records—and shows how formal methods catch these issues. The post concludes by refining the validity assertions to match real-world requirements: migrations should preserve validity, and the new schema should only allow states that would have been valid in the old schema.

Key Insight: Performance isn't a luxury or premature optimization—at sufficient scale, a quarter-second lag can be the difference between software that saves lives and software that sits unused while people die from preventable errors.

The author reflects on his EMT training experience where he discovered that electronic patient care reports (ePCRs), despite being objectively better than paper in almost every way, went unused because of a quarter-second lag on interactions. This seemingly trivial performance issue meant EMTs stuck with error-prone paper forms. At the scale of 30 million PCRs filed annually in the US, even small inefficiencies or error rates translate into lost doctor-hours and potentially lost lives. The post argues that performance isn't just a technical concern but a moral one when software operates at scale.

Key Insight: PRISM demonstrates the fundamental tension in formal tools between analytical power and practical expressivity—its ability to check complex probabilities comes at the cost of a language so limited that few real problems can be cleanly modeled in it.

Hillel Wayne explores PRISM, a probabilistic modeling language that can express statistical properties like average times and probability distributions—capabilities that TLA+ and Alloy lack. Using a game theory example of two players with different skill levels, he demonstrates how PRISM can calculate win probabilities and optimal handicaps. However, he concludes that PRISM's severe expressivity limitations—no tuples, arrays, functions, or even strings—make it impractical for most real-world problems despite its powerful probability checking capabilities.

Key Insight: Vim's power lies not in modal editing philosophy but in the sheer density of special-purpose commands packed into available keystrokes, though this same density creates discoverability problems that leave users stumbling onto essential features years too late.

This post catalogs intermediate-level Vim tricks that fall between beginner tutorials and expert deep-dives. Wayne argues that Vim's power comes not from modal editing but from its density of special-purpose tools crammed into every available keystroke. He divides Vim users into 'purists' who keep minimal configuration and 'exobrains' who customize extensively. The article covers visual mode operators, Ex commands like :g and :norm, statusline customization, autocommands, and useful plugins, all presented as discrete tricks rather than a cohesive system.

Key Insight: The history of OOP is a synthesis of many contributors solving different problems, and retroactive claims about what it 'really means' don't hold up against primary sources.

This post debunks the persistent myth that Alan Kay invented objects, tracing the concept back to Simula, which the Smalltalk team explicitly acknowledged as inspiration. Wayne examines Kay's own contradictory statements over the years and argues that the modern revisionist view that OOP is 'really about messages, not objects' doesn't match the historical record. The post emphasizes that Smalltalk's genuine innovations—like everything being an object and the doesNotUnderstand mechanism—are distinct from inventing the core concept. Wayne concludes that different OOP pioneers solved different problems, and our modern understanding is a synthesis of many contributors' ideas.

Key Insight: When modeling adversaries or environmental effects, separate your specification into controllable 'machine' and uncontrollable 'world' components, then explore what weaker-but-still-useful properties you can guarantee when full stability is impossible.

This post demonstrates how to model adversaries and environmental effects in TLA+ specifications. Wayne shows how to compose a 'machine' (the system we control) with a 'world' (outside forces we can't control) and explores what properties can still be guaranteed. The key insight is that while stability (staying in goal forever) may be impossible with adversaries, we can still prove weaker but useful properties like resilience (eventually returning to goal) or finite-spite stability. The post also shows how to verify that the machine itself never violates safety invariants, even if the world can.

Key Insight: The best property tests encode the mathematical definition of correctness rather than implementation-specific checks, but finding that definition requires understanding what makes your function unique among similar operations.

The post examines how property-based testing with contracts can catch subtle bugs that manual unit tests miss, using a buggy Python mode() function as a case study. The bug—treating 0 as falsy when checking for an uninitialized max value—only surfaces with specific input combinations unlikely to appear in hand-written tests. Wayne walks through progressively sophisticated contract approaches: type checks (unhelpful), sanity checks (partial), comparing against first element (catches bug), and testing the mathematical definition (most robust). He also explores metamorphic properties like sorting preservation and affine transformations, showing how different approaches trade off between power and overconstraint.

Key Insight: Metamorphic testing unlocks practical testing of complex systems by checking that relationships between transformed inputs hold, rather than requiring expensive or impossible-to-obtain test oracles.

Metamorphic testing is a powerful testing technique that compares outputs across transformed inputs rather than checking against known answers. Unlike traditional oracle-based tests or property-based testing, metamorphic testing leverages 'metamorphic relations' - properties that should hold between related inputs and their outputs. The technique is especially valuable for complex systems like speech-to-text where generating test oracles is expensive or impossible. Despite impressive academic case studies across many domains, the technique remains obscure because nearly all research is locked behind academic paywalls.

Key Insight: Formal specifications provide the most value not through exhaustive verification but by forcing precise thinking about designs, making subtle bugs obvious before they reach code.

This guide argues that formal specifications are practical tools for everyday software engineering, not just for building new systems from scratch. Wayne presents specifications as high-level, partial, and imperfect documents that exist apart from code and complement (rather than replace) testing. He outlines a progression of specification uses from documenting existing systems to building new ones, emphasizing that most benefit comes from clarifying understanding and catching design bugs early. The post also honestly addresses when specs aren't worthwhile: low-cost errors, implementation-level code, ambiguous requirements, and human-in-the-loop systems.

Key Insight: Formal modeling tools like Alloy can mechanically solve logic puzzles while also revealing subtle flaws in 'classic' solutions that human reasoning might miss.

This post demonstrates how to use Alloy, a formal modeling tool, to systematically solve Knights and Knaves logic puzzles rather than relying on manual reasoning. Wayne walks through the Alloy syntax for modeling these puzzles, where Knights always tell the truth and Knaves always lie, showing how the model-finder can discover all valid solutions. The post explores increasingly complex variations, including the famous fork-in-the-road puzzle and an advanced version with drunk/sober modifiers. Along the way, Wayne reveals counterintuitive results, such as how the famous fork puzzle solution only works in a special case, while a simpler general solution exists.

Key Insight: Formal methods remain niche not because they don't work, but because code verification is prohibitively expensive for most cases while design verification—though technically easier—faces cultural resistance from programmers who don't trust non-code artifacts.

This post provides a comprehensive historical overview of why formal methods remain niche in software engineering despite their potential benefits. Wayne distinguishes between code verification (proving code matches specifications) and design verification (proving system designs are correct), explaining that code verification is technically difficult—requiring extensive mathematical proofs that even with modern SMT solvers yield only about four lines of verified code per day. Design verification is technically easier but faces cultural barriers: programmers don't trust artifacts that aren't code and don't believe specification provides value beyond existing practices like pseudocode or TDD. The post argues that while full formal verification is rarely economical, partial verification and design specification offer practical value that most of the industry overlooks.

Key Insight: Security incidents in software ecosystems cannot be prevented by assigning blame to individuals; they require examining and addressing the systemic properties—cultural, technical, and organizational—that made the failure possible in the first place.

The post applies Nancy Leveson's STAMP (System-Theoretic Accident Model & Processes) framework to analyze the event-stream npm package compromise, where a malicious actor gained maintainer access and injected code to steal Bitcoin wallets. Rather than seeking a single 'root cause' to blame, STAMP reveals how the accident emerged from systemic properties: npm's ecosystem of thousands of small packages maintained by individuals who never expected responsibility, transitive dependencies that obscure accountability, lack of privilege restrictions in JavaScript, and inadequate tooling for auditing. The analysis identifies 15+ system-level factors that made the attack possible, arguing that fixing any single 'root cause' won't prevent similar attacks without addressing the deeper structural issues.

Key Insight: Technical interviews should test the skills programmers actually use daily—reading code and communicating about changes—rather than artificial whiteboard exercises that don't reflect real work.

Hillel Wayne proposes replacing traditional technical interviews with a code review exercise where candidates study a codebase, then write comments on a pull request. This approach addresses nine specific problems with conventional interviews: time investment, stress, objectivity, granularity, bias, inaccuracy, scope, communication, and calibration. The PR review can be graded against a rubric, done double-blind to reduce bias, and produces artifacts useful for data analysis. Wayne acknowledges weaknesses including setup costs, requiring candidate prep time, and not testing code-writing ability directly.

Key Insight: TLA+ is most valuable not for verifying exotic consensus algorithms but for modeling the everyday distributed systems problems engineers actually face, like message queue semantics and deduplication logic.

This post demonstrates how to model message queues and pub-sub systems in TLA+, providing practical examples that go beyond the typical consensus algorithm tutorials. Hillel walks through implementing an SQS-like queue with writers and readers, then extends it to handle at-least-once delivery semantics with message duplication and retry logic. He then shows a pub-sub variant where each reader has their own queue, including subscription management. The post emphasizes that TLA+ is useful for everyday distributed systems problems, not just verifying Paxos, and calls for more accessible learning resources.

Key Insight: Powerful formal verification tools like TLA+ don't have to be hard to learn—the barrier is pedagogical, not technical.

Hillel Wayne announces the release of his book 'Practical TLA+', a comprehensive introduction to the formal specification language TLA+. He explains that TLA+ allows developers to write blueprints of systems and find complex bugs in minutes rather than days or weeks. The book is structured in two parts: the first covers syntax and semantics, while the second focuses on practical application techniques. Wayne emphasizes that the book is designed to be accessible, with extensive editing to ensure clarity at every step.

Key Insight: Constraint programming optimization is deeply nonlinear—improvements depend on solver choice, other constraints, and dataset, so systematic experimentation matters more than following rules.

This tutorial walks through optimizing a MiniZinc conference scheduling model, demonstrating how to reduce runtime from over 8 hours to just 2 seconds through various techniques. Wayne explores solver selection, constraint reformulation, symmetry breaking, and channeling while discovering that optimization is highly nonlinear—what helps with one solver or dataset may hurt with another. The key breakthrough comes from using channels to decompose the schedule into separate talk_time and talk_room arrays, combined with precomputing favorites and using native functions like nvalue instead of hand-rolled constraints.

Key Insight: Constraint solvers are underappreciated tools that let you express complex optimization problems declaratively, though making them scale requires deep expertise in heuristic optimization.

This tutorial introduces MiniZinc, a constraint solving language for modeling optimization problems, using a conference scheduling problem as the main example. The post walks through defining enums, parameters, decision variables, and constraints to create a schedule that maximizes attendee satisfaction. Wayne demonstrates how constraint languages make it easy to add new requirements—like ensuring speakers don't present twice on the same day—without rewriting the core algorithm. However, he notes that while expressing constraints is straightforward, optimizing models for real-world scale is challenging and poorly documented, which sets up a follow-up article on optimization techniques.

Key Insight: Formal methods don't replace testing and other Agile practices—they augment them by catching design-level bugs in concurrent systems that testing fundamentally cannot find efficiently.

Hillel Wayne demonstrates how formal methods can dramatically outperform traditional testing for finding concurrency bugs. He revisits the famous Extreme Programming Challenge Fourteen, where Agile practitioners struggled for weeks to find a bug in a bounded buffer implementation. Using TLA+, Wayne finds the same bug in just 31 minutes, compared to the 16+ hours it took the original challengers—and he argues the true comparison is even more favorable since the testers couldn't reliably detect if their fixes worked. The post concludes that formal methods should augment, not replace, Agile practices like testing and pairing.

Key Insight: Decision tables are an accessible formal specification technique that makes complex conditional logic easy to reason about, verify, and communicate, yet they've become needlessly obscure.

Decision tables are a simple but underused formal specification technique for representing branching logic, where inputs map to exactly one output row. Wayne explains the concept in under two minutes, then demonstrates its practical value through a real-world migration of a legacy audio system with complex conditional logic involving text-to-speech, manual uploads, and database lookups. The table format made it easy to reason about edge cases like 'what happens if we have a legacy override pointing at a manual upload?' Decision tables can also reveal properties like input irrelevance and decomposition opportunities, and can be expanded into test suites.

Key Insight: The languages developers actually use are often inadequate for expressing the precise specifications that real systems require.

Hillel Wayne shares an excerpt from Michael Jackson's book 'Software Requirements and Specifications' that challenges developers to honestly inventory the languages they use and test whether those languages can express common specification statements. The excerpt presents ten diverse requirements—from physical constraints on elevators to temporal conditions on vending machines—and asks readers to consider how they would formally express each. The implicit argument is that most developers lack adequate languages for expressing precise specifications, revealing a gap in our tooling for requirements engineering.

Key Insight: Claims about programming paradigms being universally easier to reason about collapse under empirical testing - formal verification difficulty depends on the specific problem, not the paradigm.

Hillel Wayne challenged the common assertion that functional programming is inherently easier to reason about than imperative programming by asking people to formally prove the correctness of three functions (Leftpad, Unique, and Fulcrum). The results showed that formal verification is difficult in both paradigms, with many FP advocates unable to complete proofs they initially dismissed as trivial. The formal verification community responded enthusiastically with solutions in numerous languages, while critics who claimed FP superiority without providing proofs had no overlap with those who actually completed the challenge. Wayne concludes that which paradigm is easier to reason about depends heavily on the specific problem domain rather than being a universal truth.

Key Insight: The use of '=' for assignment—now ubiquitous—was not a natural or obvious choice but rather an accident of history stemming from CPL's complexity, BCPL's simplifications, and Ken Thompson's preference for shorter code.

The post traces the historical evolution of the equals sign as an assignment operator, starting from the four dominant languages of the early 1960s (COBOL, FORTRAN, ALGOL-60, and LISP). While ALGOL and its descendants used ':=' for assignment and '=' for equality, the shift began with CPL's introduction of '=' for initialized definitions, continued through BCPL's simplifications, and culminated in B where Ken Thompson chose '=' for all assignment purely because it's shorter than ':='. C inherited this convention, and most modern languages follow C's lead despite ':=' being the more historically common and semantically clearer choice.

Key Insight: The fundamental tradeoff in testing is between automanual tests that give complete information about specific cases and generative tests that give partial information across much wider state spaces.

This post provides a comprehensive taxonomy of automated testing approaches, dividing them into automanual tests (where humans specify exact inputs and outputs) and generative tests (where programs search for failing inputs). Wayne walks through unit tests, integration tests, acceptance tests, feature tests, diff tests, and parameterized tests in the automanual category, then covers property tests, fuzz tests, and model tests in the generative category. He argues that while automanual tests are easier to write and deterministic, they only test tiny slivers of state space, whereas generative tests explore much wider ranges at the cost of specificity. The piece serves as both reference guide and gentle critique of testing orthodoxy.

Key Insight: Formal specification isn't just for finding bugs—it's a powerful tool for understanding problem domains, as modeling a package manager quickly reveals why Nix's isolated dependency approach solves real reproducibility problems.

Hillel Wayne uses the Alloy specification language to formally model package managers and demonstrate why Nix's 'purely functional' approach solves real problems. He starts with a naive package manager that fails when upgrading shared dependencies, then shows how allowing multiple versions prevents breakage. The key insight comes when modeling the gap between developer and user environments: traditional package managers can fail because developers don't explicitly track all transitive dependencies. Nix solves this by coupling each requirement to its specific program, creating isolated dependency trees that guarantee reproducible builds across machines.

Key Insight: TLA+ suffers from an example gap—real-world usage tends to be proprietary and complex, leaving learners without accessible intermediate examples to bridge the gap from toys to production specifications.

The post addresses a common complaint about learning TLA+: the lack of accessible examples between trivial toy problems and complex industrial algorithms. Wayne explains this gap exists because TLA+ is typically used to design complicated systems, often proprietary ones, and the community is very small. He introduces a curated list of beginner-to-moderate complexity industrial examples, excluding those already in standard resources. The post serves as a practical resource for learners seeking real-world TLA+ specifications.

Key Insight: The many ways monad tutorials fail—overwrought formalism, strained analogies, dismissive oversimplification—are the same ways we fail to explain any programming concept.

This satirical post presents absurd explanations of basic programming concepts in the style of bad monad tutorials. Wayne demonstrates how explanations can fail by being either overly abstract and mathematical, using bizarre analogies, oversimplifying to the point of inaccuracy, dismissing the importance of understanding, or being needlessly jargon-heavy. The post serves as a critique of how programming education often goes wrong, using the notorious difficulty of monad tutorials as its framing device.

Key Insight: APL languages need better organization of their primitives—by complexity level, problem domain, and reusable idioms—to transform them from powerful-but-opaque tools into learnable, practical languages.

Hillel Wayne argues that the biggest problem with APL-family languages isn't their cryptic symbols or write-only reputation, but discoverability—finding the right primitive among hundreds of options is extremely difficult. Using J as an example, he shows how a 22-character solution took 40 minutes to write because he had to search through 200 primitives to find the right combination. He proposes three solutions: labeling primitives by complexity level, categorizing them by problem domain, and creating a library of reusable components and idioms. These changes would make APLs more learnable and code more readable by letting programmers recognize common patterns.

Key Insight: Complex software debates cannot be settled by reasoning alone because cascading impacts through interconnected systems exceed human cognitive capacity—only empirical studies can reveal actual outcomes.

The post argues that programmers cannot reason their way to answers about complex debates like static vs dynamic typing because software development is a system with countless interconnected impacts. Direct impacts lead to linear first-order effects, which cascade into second-order effects, and everything becomes nonlinear when factors change the rate at which other factors affect outcomes. The author contends that the human mind simply isn't powerful enough to trace all these cascading effects, comparing the challenge to the unsolvable three-body problem in physics. While humans develop useful heuristics and intuitions, these are context-dependent and don't generalize well. The solution proposed is empirical software engineering: running controlled studies to measure actual outcomes rather than reasoning from first principles.

Key Insight: Formal specification is valuable not just for verification but for understanding—modeling Redux in TLA+ revealed its essential structure more clearly than tutorials could.

This post demonstrates how to model Redux's state management pattern using TLA+, a formal specification language. Wayne walks through creating a reducer specification, then proves it 'refines' a simpler global state model by showing both systems always end up with equivalent state. He also shows how to create a temporal property that ensures all state changes go through Redux's proper channels, catching violations even when integrating with other components. The post concludes with the observation that specification helped Wayne understand Redux better than tutorials did.

Key Insight: The 'unthinkable' programming paradigms that critics claim we're missing have already been thought and implemented—we just don't recognize them because they don't fit our narrative of what counts as serious computer science.

Hillel Wayne responds to Tomas Petricek's argument that modern programming language theory makes restrictive assumptions that prevent us from seeing alternative paradigms. Wayne argues that Petricek's two proposed 'unthinkable' paradigms—taxonomic programming and metaphorical programming—are not actually unthinkable at all. He demonstrates that taxonomic programming was extensively explored during the OOP 'method wars' of 1980-1995 and was formalized through contracts and Hoare logic. Metaphorical programming, he argues, exists in APL languages (which use primitives to shape thought) and in DSLs like Inform 7. His conclusion is that these paradigms aren't incommensurate alternatives—they're already present in programming, just underappreciated.

Key Insight: When teaching abstractions that leak, the solution isn't to dump prerequisites or accept inferior workarounds, but to find independent contexts where each prerequisite becomes naturally useful before synthesis is needed.

The author discusses pedagogical challenges when teaching TLA+ through the PlusCal abstraction layer. While PlusCal simplifies syntax significantly, certain advanced concepts like temporal invariants require underlying TLA+ knowledge that isn't otherwise needed in PlusCal. Rather than either using clunky workarounds or dumping inapplicable concepts on readers, the author explores a third approach: finding ways to make each prerequisite concept independently useful within PlusCal contexts, then synthesizing them later when needed.

Key Insight: The tech industry's habit of citing only three women when discussing CS history obscures the many other women who made foundational technical contributions to the field.

This post introduces a curated list of important women in computer science beyond the commonly cited figures of Grace Hopper, Margaret Hamilton, and Ada Lovelace. Wayne establishes criteria for inclusion: specific identifiable contributions, technical (not social/political) achievements, and historical work predating 1997. The post serves as an introduction to a sampler list rather than an exhaustive compilation, acknowledging the author's limitations in covering contributions outside his specialties.

Key Insight: Alloy's relational algebra foundation makes it ideal for quickly verifying properties of data structures and item relationships, even if the problem domain (game randomizers) isn't its intended niche.

This post demonstrates how to use Alloy, a lightweight formal methods tool, to verify that randomized game configurations are always winnable. Using Link to the Past Randomizer as an example, Wayne builds an Alloy model that represents chests, items, and their requirements, then formally proves that certain placement restrictions guarantee the game can be completed. The post progressively refines the model to handle increasingly complex scenarios: unique item placement, requirement cycles, multi-item requirements, and alternative puzzle solutions. Wayne concludes by comparing Alloy favorably to TLA+ for its simplicity and speed, while noting its limitations for dynamic systems and concurrency.

Key Insight: The value of software engineering research lies not in exciting conclusions but in methodological rigor that makes any conclusion—even a null result—trustworthy.

Wayne highlights an obscure software engineering paper about abbreviated vs. full-word identifier names as exemplary research methodology. Despite its mundane-sounding topic, the paper demonstrates exceptional rigor: a comprehensive literature review, mixed qualitative and quantitative methods, objective defect measurement through deliberately seeded faults, and meticulous experimental design that addresses nearly every threat to validity. The researchers tested 100 participants across experience levels, used real codebases, and followed up with ethnographic observation. The surprising finding—no significant difference between abbreviated and full names—is made credible by the methodology's thoroughness.

Key Insight: Vim macros derive their power from being plain text keystrokes stored in registers, making them both infinitely flexible and trivially editable—but knowing when not to use them is just as important as knowing how.

This post explains why Vim's macro system is uniquely powerful: macros are simply stored keystrokes in registers, giving them complete access to all Vim functionality. Wayne provides practical techniques for recording, editing, and debugging macros, along with useful settings and commands that enhance macro usage. He covers marks, registers, visual mode, and conditionals within macros, while cautioning that complex recursive macros often indicate you should use a different tool entirely. The post serves as a practical companion to Vim's sparse official macro documentation.

Key Insight: Using contracts as PBT invariants creates self-documenting integration tests where the contracts do the verification work and testing becomes pure fuzzing.

The post demonstrates how combining property-based testing (PBT) with contracts can create effective integration tests. Contracts define preconditions and postconditions that serve as PBT invariants, eliminating the need to manually specify test assertions. When PBT generates inputs matching preconditions, contracts automatically verify correctness throughout the call chain. The author shows this through a list removal example and a siteswap validator, illustrating how contracts 'chain' through function calls to provide integration-level verification. This approach addresses PBT's challenge of coming up with invariants and integration testing's complexity of orchestrating components.

Key Insight: Case studies are the most practical form of rigorous evidence for technology decisions because they represent real tradeoffs and, unlike formal research, can be produced by working engineers from their everyday experiences.

The post examines what it actually means to choose 'the right tool for the job' by analyzing different ways we evaluate technology choices. Wayne walks through a hierarchy of evidence: requirements, personal experience, authority, abstract arguments, examples, case studies, and formal research. He argues that personal experience and authority are unreliable due to cognitive biases, while abstract arguments often cancel each other out. Case studies emerge as the practical gold standard, being more rigorous than examples but more accessible than formal research. The conclusion is that laypeople can and should produce case studies from their own work to help the community make better decisions.

Key Insight: The real enemy of code readability isn't comments or extracted methods—it's context switching, and sometimes a 'what' comment is the most direct way to keep information where it's needed.

The post challenges the conventional wisdom that comments should only explain 'why' and not 'what'. Wayne argues that the real issue is context switching—whether that's looking up variable meanings, digging through git blame, or jumping between extracted methods. He critiques the 'Extract Till You Drop' style of clean code, showing how aggressive method extraction can actually harm readability by forcing readers to jump around. The core argument is that keeping information where it's needed—sometimes via 'what' comments—reduces cognitive load better than either cryptic code or over-extracted methods.

Key Insight: Microservices and classes are structurally identical - microservices only provide better separation of concerns because they enforce interfaces that programming languages fail to enforce.

The post introduces a simple visual notation of 'boxes, arrows, and ports' to analyze software architecture, revealing that classes and microservices are topologically equivalent from a design perspective. Wayne argues that the key difference is the size of the largest 'proper interface' - Ruby's biggest enforced boundary is the class, while microservices enforce boundaries at the service level via HTTP APIs. He concludes that microservices' separation of concerns is essentially using devops to compensate for programming language limitations, and that choosing microservices primarily for this benefit is misguided.

Key Insight: Contracts occupy a distinct correctness niche from types and tests by expressing runtime invariants and inter-parameter relationships at function boundaries, making implicit assumptions explicit and localizing bugs to their source.

This post builds up the concept of contract programming from first principles, distinguishing it from type checking and unit testing. Starting with a simple number-guessing game, Wayne demonstrates how preconditions and postconditions can enforce correctness at function boundaries. He argues that while Python's assert statements are crude, they capture the essential idea: contracts specify what callers must guarantee and what functions promise in return. The post surveys contract support across languages, from inadequate library-based solutions to D's built-in support to Eiffel's gold-standard implementation, ultimately encouraging developers to make implicit contracts explicit even without native language support.

Key Insight: Array programming languages like J represent a 'Specific Purpose Language' paradigm that trades general-purpose features for exceptional expressiveness in numerical computation.

Hillel Wayne demonstrates how to calculate personal burn rates using J, an array programming language, as he prepares to leave work for EMT training. The post walks through increasingly complex financial calculations: simple division for basic burn rate, tables for comparing multiple scenarios, and rank-3 arrays for tracking savings over time with variable income. He shows how J's native support for arrays and rank operations makes these multi-dimensional calculations concise compared to traditional languages. The post concludes with a reflection on how J represents a 'Specific Purpose Language' optimized for numerical computation rather than general programming tasks.

Key Insight: TDD is likely useful but should be part of a diverse correctness toolkit, and we should compare techniques to each other rather than to doing nothing.

Hillel Wayne responds to Eric Smith's 'Why TDD is Crap' talk, systematically addressing each criticism while maintaining that TDD is likely a useful correctness technique. He examines the limited empirical evidence (notably the Nagappan study showing 60% defect reduction at 25% time cost), acknowledges TDD's limitations, and argues it should be part of a broader correctness toolkit alongside contracts, property-based testing, and upfront design. The post emphasizes that comparing TDD to 'nothing' is the wrong framing—we should compare it to other correctness techniques, each with tradeoffs. Wayne concludes that while we don't know much about what good software engineering looks like, TDD probably helps, and we shouldn't mock those who disagree with our preferred techniques.

Key Insight: Unit tests verify that code units work in isolation, but since programs exhibit emergent complexity from component interactions, unit tests are better understood as development scaffolding than as actual tests of program correctness.

Wayne argues provocatively that unit tests shouldn't be classified as 'tests' but rather as 'development' activities. His reasoning centers on emergence: while unit tests verify individual components work in isolation, programs exhibit complex behaviors arising from component interactions that unit tests cannot capture. Since unit tests don't verify the actual program behaves correctly—only that isolated code units do—they belong to the development phase rather than the testing phase. This reframing has implications for how we think about Agile vs Waterfall, the role of QA engineers, and what real testing should look like.

Key Insight: Software correctness requires combining every available technique—unit tests, type systems, static analysis, formal methods—because humans inevitably make mistakes and no single tool catches more than a narrow slice of possible errors.

Hillel Wayne critiques Robert 'Uncle Bob' Martin's dismissive attitude toward software correctness techniques beyond unit testing. Martin argues that 'discipline' rather than tools is the solution to software problems, but Wayne contends this is naive—modern systems engineering recognizes that humans inevitably make mistakes, so we must design systems that catch errors rather than blame programmers. Wayne demonstrates through code examples how unit tests alone miss floating-point edge cases, null paths, and security vulnerabilities that other techniques like property-based testing, type systems, and static analysis would catch. The core argument is that no single technique is sufficient; we need every tool available because 'there's only one way a program is right and infinite ways a program can be wrong.'

Key Insight: When trying to convince rather than merely explain, your examples must demonstrate why something matters, not just what it is—and achieving that balance of simplicity and complexity requires deliberate craft.

The post argues that examples in persuasive writing must match the writer's intent—instructive examples teach what something is, while persuasive examples demonstrate why it matters. Using a unit testing article as a case study, Wayne shows how a trivial 'add' function fails to convince skeptics because it doesn't reveal testing's actual benefits. He then constructs a better example using string parsing for citation coauthorship, demonstrating how tests catch subtle bugs like non-commutativity and edge cases that aren't obvious from reading code. The core message is that persuasive examples require significantly more craft than instructive ones.

Key Insight: Scientific code quality is a social problem masquerading as a technical one—we have the tools to write better code, but no good way to convince researchers to use them.

The post examines the alarming consequences of bugs in scientific code, using the infamous Reinhart-Rogoff Excel error as a case study where a coding mistake influenced real austerity policies affecting Greece. Wayne argues that scientists lack the training and motivation to write rigorous code, yet their buggy analyses drive major policy decisions. He acknowledges that technical solutions exist but frames this fundamentally as a social problem—convincing non-programmers to adopt boring, frustrating practices for nebulous benefits. His tentative suggestion is mandatory code sharing with papers, though he admits this has significant practical barriers.

Key Insight: Oracle functions let you leverage existing correct implementations—whether slow, partial, or soon-to-be-replaced—as test references, turning the apparent redundancy of 'testing against something you already have' into a powerful verification strategy.

The post introduces the concept of oracle functions in property-based testing with Hypothesis, demonstrating how known-correct functions can validate new implementations. Wayne presents four oracle patterns: using original functions during refactoring, leveraging special-case oracles that work on restricted domains, employing inefficient but correct implementations as references, and generating test inputs from expected outputs via reverse oracles. The approach complements traditional unit tests by providing broader coverage through randomized input generation. Wayne emphasizes that while oracles add testing complexity, they catch subtle bugs that might escape conventional tests.

Key Insight: Effective skepticism in programming requires not just disagreement but deep comprehension of opposing views, rigorous evidence, and enough intellectual honesty to acknowledge when your own work falls short.

Wayne curates a list of programming articles that challenge mainstream beliefs, from skepticism about formal methods to defenses of PHP. He argues that good skeptical articles are rare because they require deep knowledge of both why people believe something and why it fails. The post establishes four criteria for quality skeptical writing: controversial stance, genuine understanding of the opposition, rigorous argumentation with data, and respectful tone. Wayne includes anti-examples for each criterion, including one of his own articles, demonstrating intellectual honesty about the difficulty of meeting these standards.

Key Insight: Formal specification lets you find concurrency bugs in deployment systems before writing any code by exhaustively checking all possible orderings of operations.

This post demonstrates how to use TLA+ to model and verify a zero-downtime deployment system. Starting with a naive approach that immediately fails verification, Wayne iteratively builds a correct specification by adding a load balancer, update flags, and a coordinator process. The model checker exhaustively explores all possible orderings of concurrent server updates to find bugs. The final spec ensures both safety properties: at least one server is always accessible, and all accessible servers run the same code version.

Key Insight: Doctests uniquely detect documentation bugs rather than code bugs—when they fail but unit tests pass, your docs are lying about what the code does.

Doctests are a unique Python feature that embeds tests directly in documentation strings, simulating REPL interactions to verify examples work correctly. While they've fallen out of favor because they lack setup mechanisms and don't scale well compared to unit tests, Wayne argues they serve a fundamentally different purpose: detecting documentation bugs rather than code bugs. When a doctest fails but the unit test passes, it signals the documentation is out of sync with the code's actual behavior. Wayne sees doctests as an underexplored approach to keeping documentation consistent with code, inverting the common pattern of generating docs from code.

Key Insight: Sometimes the best use of a technical writing format is to remind us that all dogs are good dogs.

This satirical piece parodies the popular 'Falsehoods Programmers Believe' format by applying it to dogs instead of technical topics. Rather than exposing edge cases in date handling or name validation, Wayne constructs a playful logical argument that all dogs are good dogs, all dogs are the best dogs, and nothing is better than dogs. The piece subverts reader expectations by using a technical writing format for pure wholesome content about canine appreciation.