buttondown-com-hillelwayne

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.

Hillel Wayne published a new blog post titled "Some Silly Z3 Scripts I Wrote" after five months without updates. The post discusses Z3 solver examples and mentions material that didn't make it into his upcoming book "Logic for Programmers." He also notes he's winding down gated content on Patreon.

The author is skipping this week's newsletter and offering ten free copies of "Logic for Programmers." Five copies are available immediately, while the other five had technical issues with availability timing.

The author analyzes AI-generated formal specifications, finding they often contain obvious, tautological properties rather than subtle, meaningful ones. While AI can help beginners create specs, it struggles with complex verification properties like liveness conditions. The article questions whether AI truly lowers the skill threshold for effective formal methods use.

The article argues that while companies should choose "boring" technology for mission-critical systems due to high maintenance costs, they can be more innovative with development practices and tools. Practices and tools are easier to adopt and abandon than core technology infrastructure, which creates long-term maintenance burdens when using new technologies.

The author discusses Chicago vs New York pizza debates, noting that most Chicago pizza chains serve stuffed pizza rather than deep dish. The article argues that Chicago is a great sausage city, with even Home Depot stores selling hot dogs.

The article argues that a comprehensive specification is not necessarily code, as a spec corresponds to a set of possible implementations while code is a single implementation. Specifications are abstractions of code, and even detailed specs that can generate programs remain distinct from code itself.