buttondown-com-hillelwayne

The author argues that while no single math field has high ROI for the average programmer, each developer works in a domain where some branch of math could help. They suggest broad exposure to many fields (e.g., via textbooks) is more practical than deep study of one topic, since you need to know a field exists before deciding to learn it in depth.

Adding assumptions to a formal property makes it logically weaker—guaranteed to work in fewer cases. Engineers add assumptions when stronger properties are impossible, too costly, or unverifiable. These assumptions often involve factors outside the program, like the operating environment or external dependencies.

LaTeX and Inkscape define a "point" differently: LaTeX uses 1/72.27 inch (Knuth's TeX standard), while Inkscape uses 1/72 inch (from PostScript and CSS). The difference traces back to historical variations in typographic measurement standards.

Version 0.14 of "Logic for Programmers" is out, with print copies targeted by end of June. In August, the author starts at Antithesis as a developer educator. The newsletter will shift focus and may become less frequent.

The article distinguishes between illegal states (states a system must never be in) and unwanted states (states that are acceptable temporarily but must be resolved). It argues that many states engineers try to make illegal—like scheduling conflicts or overbooking—are actually unwanted, and systems need to represent them because external inputs and workflows sometimes require them.

The article discusses how TLA+ semantics guarantee nonordering of statements, but model checkers like TLC implement practical constraints that can break these guarantees. This creates confusion when using effectful operators like PrintT and Assert, which introduce side effects not present in pure TLA+ semantics.

The article explains logical quantifiers (universal "all" and existential "some") and their application in software development. It demonstrates how quantifiers simplify code patterns, express software properties like sorted lists, and enforce database invariants through duality transformations.

The self-published book "Logic for Programmers" has sold 1,180 copies and generated $18,241 in royalties since its release one year ago. The author plans to complete major rewrites by summer, with graphic design and copy editing scheduled for autumn, aiming for a final 1.0 release in winter.

The author challenges the common belief that writing speed isn't a programming bottleneck, suggesting faster writing could enable new development processes. They argue that dramatically increased typing speed would make boilerplate trivial and allow more speculative editing and tool creation. Current development practices may be shaped by existing writing speed constraints.

The article discusses programming language "escape hatches" - features that deliberately break core language assumptions to add capabilities. It cites examples like Rust's unsafe mode, C++ inline assembly, and Ruby's send method. Escape hatches are necessary but problematic as they can cause incorrect behavior when language assumptions are violated.

The article explores a conceptual model of arrays as mathematical functions, explaining how one-dimensional arrays map indices to values. It extends this to multidimensional arrays via currying and contrasts arrays with tables, which handle heterogeneous data through struct-of-arrays representations.

The author discusses software books they wish existed, including topics like configuration management, complex data schemas, computer science for software engineers, MISU patterns, essential tools for developers, historical optimizations, and Sphinx documentation internals. They reflect on the unique value of books compared to blogs and online resources in software education.

The article argues that the Sapir-Whorf hypothesis does not apply to programming languages. While programming paradigms influence problem-solving approaches, this effect is better explained by the Tetris Effect—where intensive practice with any skill alters thinking patterns.

The article discusses logical duals in software engineering, where operators F and G are duals if F(x) = !G(!x). It focuses on quantifier duality between "some" and "all," showing how tools like Z3, property testing, and model checkers can use this relationship to either find values satisfying properties or check that all values satisfy them.

The article contrasts demonic nondeterminism, where systems make worst-case choices to verify properties on all paths, with angelic nondeterminism, where they make best-case choices to verify properties on any path. Angelic nondeterminism underpins complexity class NP and serves as an abstraction in declarative languages.

The article argues that many challenging LeetCode interview problems, such as the coin change problem and stock profit maximization, can be solved easily using constraint solvers like MiniZinc. These solvers handle mathematical optimization problems that are difficult to implement manually with dynamic programming or custom algorithms.

The author has published a 3500-word blog post on the early history of algebraic data types instead of the planned newsletter. They also announced they will be speaking at P99 Conf about designing low-latency systems with TLA+.

Formally verified code can still have bugs in practice due to invalid proofs, incorrect specifications, or flawed assumptions. Even when code is proven correct against a specification, the specification may not capture all desired properties or may rely on assumptions that don't hold in real-world use.

The author reflects on how skill development often occurs through sudden "phase changes" rather than gradual progress, drawing from their experience with running and programming. They explore whether these mental leaps can be accelerated or if it's more productive to motivate people to persist until the phase change occurs naturally.

Modal editing, the key feature of Vim, originated from an experimental interface at Xerox and was adapted by Bill Joy for vi to work with slow terminals. Its popularity came from being bundled with free Unix distributions rather than its inherent benefits. Despite Vim's success, modal editing remains largely confined to vi descendants and hasn't spread to other software categories.

Hillel Wayne is taking a break from writing his weekly software essay newsletter Computer Things for the rest of the year due to burnout. The writing process has become more time-consuming, taking two to three days instead of an afternoon. He plans to resume the weekly cadence in 2026.

Logic for Programmers is available at 50% off with coupon code "feedchicago" until the end of the month. All royalties from purchases using this coupon will be donated to the Greater Chicago Food Depository.

A fundraiser for the Greater Chicago Food Depository offers Logic for Programmers at 50% off, with all royalties going to charity. The campaign has raised over $1600 and runs until the end of November.

The newsletter shares various software facts, including that Tetris was implemented in Conway's Game of Life on a 30 trillion pixel grid, leap seconds will be abolished by 2035, and Vim is Turing complete. It also mentions that Cloudflare uses lava lamps for random number generation and most mergesort implementations were broken before 2006.

The Liskov Substitution Principle extends beyond inheritance to any code substitution scenario. It requires that substituted code has weaker preconditions and stronger postconditions than the original to maintain correctness. This principle applies broadly to API changes and code modifications, not just object-oriented subtyping.

The author lists several pain points with Prolog, including lack of standardized strings, no functions, limited collection types, no boolean values, confusing cut operators, and non-intuitive behavior with negation and bagof queries. These issues complicate programming tasks despite Prolog's strengths in logic programming.

The article explains how to migrate a database from a boolean 'is_activated' column to a nullable 'activated_at' column, then to an event-sourcing model, while preserving external properties through refinement mappings. It discusses how these mappings allow legacy code to continue working with transformed data, and examines mutability constraints that may affect refinement validity.

The Logic for Programmers book has released version 0.13, which is over 50,000 words and features rewritten chapters with new content and connections between topics. The author has handed the manuscript to a copy editor to prevent further additions and aims to have a printed version available before summer.

The article introduces possibility properties (P(x)) in formal methods, which indicate whether something can happen in a system model. These complement standard temporal operators A (always) and E (eventually), helping verify state reachability in specifications. However, mainstream formal tools like Alloy and TLA+ don't natively support possibility properties.

The author describes a collaborative documentation technique where complex spec changes are first written out in a markdown file to ensure mutual understanding. This approach helps bridge knowledge gaps between team members by documenting problems, solutions, and reasoning before implementing changes.