Hillel Wayne
Writer and consultant on formal methods and software correctness; author of Practical TLA+ and Logic for Programmers.
Hillel Wayne did not write this page. ppll compiled it from their own words, each linked to the source. Is this you? · Report a mistake
Latest Newsletter
What they believe
-
Almost nothing programmers believe is unique to software is actually unique to software.
Almost everything we think is unique about software appears in every other field of engineering.
hillelwayne.comSaid 20 Jan 2021This on korrents
-
Software development is separated from engineering by circumstance rather than essence, and most programmers could cross that gap without retraining.
We are separated from engineering by circumstance, not by essence, and we can choose to bridge that gap at will.
hillelwayne.comSaid 18 Jan 2021This on korrents
The bold line is korrents’ wording; the quote is theirs. These 2: what they wrote before what they said aloud, one per source, newest first.
Feed
As its own page →Hiding
22 October
30 September
16 September
1 September
18 August
29 July
From one piece Formal methods with Hillel Wayne 15 beliefs · youtube.com
-
Their words
I think the case of TLA+ and most, not all, but most formal methods, they shine the most in highly computational domains, where most of the problems are highly technical and not like business embedded.
-
Their words
And I wonder sometimes if that is the reason people don't recognize the use of math in software engineering is because the math they do need is not the math they've been exposed to.
-
Their words
But I think it is more useful for most developers to have an exposure to like what math has in the various fields versus just going all in every single field when they see them, right? You've got to know what's available to know what's most useful for you. And most math will not be useful for you.
+ 12 more
-
korrents.com
Concurrency is hard not because human brains cannot handle it but because nobody gets enough practice at it.Their words
I think a large part of the problem of why it's hard for us is because you don't get a lot of practice. Usually when you have a race condition in a system, you find out months later and then you try a fix and you find out weeks later after that if the fix actually worked.
-
Their words
Then the actual system might still have bugs, but we can iron out the issues in the abstraction such that we don't actually build them in the real system.
-
energyformal proofnuclear power
Their words
but I can tell you with first hand experience nuclear power plants do not care about this stuff. They're actually just fine with with with thorough testing.
-
Their words
when you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get correct 99% of the time is probably good enough to use in almost all cases.
-
Their words
I think this project and writing about it and thinking about it has firmly moved me from the camp of we are definitely not to we probably are.
-
Their words
And that kind of compiling of information about the materials is something other fields do that we don't do. An analogy that I would think of in software would be something like a 500-page book on how to version an API.
-
korrents.com
Software iterates better than every other engineering field and plans worse than all of them.Their words
while we are a lot better at iterating than other fields, we're worse at the planning part. Like we still need to do some kind of planning before we iterate and we just aren't as good as those other fields.
-
korrents.com
Version control is the one thing every traditional engineer wishes their old field had.Their words
Yeah, I interviewed like 20 people on this. I think all 20 mentioned version control as the thing they wish they had in their old field.
-
Their words
Software is kind of unique in having the third kind of the practitioner conference where we are just meeting to get better at what we do. We also are really the only kind to really focus heavily on like open source in making our knowledge freely available.
-
korrents.com
Software did not invent iterative development: mining engineers had their Agile revolution in 1960.Their words
And the first thing he pointed out to me was that they had their Agile revolution in 1960.
-
Their words
The core tension of engineering is between how expensive it is to make a mistake and how quickly you can iterate. The faster you can iterate, the less planning you need to do before you iterate, and the more expensive it is, the more planning you need to do.
-
Their words
If I had to summarize what I found in general, I'd put it like this. Everybody hates waterfall.
21 July
14 July
7 July
17 June
10 June
2 June
28 May
20 May
13 May
6 May
28 April
1 April
18 March
23 February
25 September 2025
9 September 2025
6 August 2025
-
Lovedrcmnd.app
Making Software: What Really Works, and Why We Believe ItTheir words
But no blog post has influenced me as profoundly as Data and Reality or Making Software. There is no blog or talk about debugging as good as the Debugging book.
7 May 2025
1 April 2025
12 March 2025
4 March 2025
3 February 2025
11 September 2024
15 July 2024
17 June 2024
29 May 2024
14 May 2024
1 May 2024
10 April 2024
5 January 2024
21 August 2023
18 May 2023
7 April 2023
Nothing matches.
Beliefs
Korrents What they believe 45 beliefs — each backed by an exact quote.
Each is a — compiled by korrents.com, not by them: the one-line wordings are korrents', the quotes are theirs.
Recent
Every branch of engineering hates waterfall, not just software.
If I had to summarize what I found in general, I'd put it like this. Everybody hates waterfall.
Formal methods with Hillel Wayne Said 29 Jul 2026
The core tension of all engineering is between how expensive a mistake is and how quickly you can iterate, and that alone decides how much planning a field does.
The core tension of engineering is between how expensive it is to make a mistake and how quickly you can iterate. The faster you can iterate, the less planning you need to do before you iterate, and the more expensive it is, the more planning you need to do.
Formal methods with Hillel Wayne Said 29 Jul 2026
Software did not invent iterative development: mining engineers had their Agile revolution in 1960.
And the first thing he pointed out to me was that they had their Agile revolution in 1960.
Formal methods with Hillel Wayne Said 29 Jul 2026
Show 42 more
Software is the only field of human labour with practitioner conferences and freely shared knowledge; every other field has only academic conferences and trade shows.
Software is kind of unique in having the third kind of the practitioner conference where we are just meeting to get better at what we do. We also are really the only kind to really focus heavily on like open source in making our knowledge freely available.
Formal methods with Hillel Wayne Said 29 Jul 2026
Version control is the one thing every traditional engineer wishes their old field had.
Yeah, I interviewed like 20 people on this. I think all 20 mentioned version control as the thing they wish they had in their old field.
Formal methods with Hillel Wayne Said 29 Jul 2026
Software iterates better than every other engineering field and plans worse than all of them.
while we are a lot better at iterating than other fields, we're worse at the planning part. Like we still need to do some kind of planning before we iterate and we just aren't as good as those other fields.
Formal methods with Hillel Wayne Said 29 Jul 2026
Other engineering fields compile deep reference books about their materials and software has nothing of the kind, not even a five-hundred-page book on how to version an API.
And that kind of compiling of information about the materials is something other fields do that we don't do. An analogy that I would think of in software would be something like a 500-page book on how to version an API.
Formal methods with Hillel Wayne Said 29 Jul 2026
Software developers probably are engineers after all, on the evidence of the people who did both jobs -- though that research was done before LLMs.
I think this project and writing about it and thinking about it has firmly moved me from the camp of we are definitely not to we probably are.
Formal methods with Hillel Wayne Said 29 Jul 2026
Formal methods are not used everywhere because for most real problems writing down what the function should do is itself a nightmare, and a program that is right ninety-nine per cent of the time is good enough.
when you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get correct 99% of the time is probably good enough to use in almost all cases.
Formal methods with Hillel Wayne Said 29 Jul 2026
Nuclear power plants, the standard example of software that must be proved correct, do not care about formal verification: thorough testing is enough for them.
but I can tell you with first hand experience nuclear power plants do not care about this stuff. They're actually just fine with with with thorough testing.
Formal methods with Hillel Wayne Said 29 Jul 2026
Verifying a simplified model rather than the real system is worth doing even though the real system will still have bugs, because the bugs you designed in never get built.
Then the actual system might still have bugs, but we can iron out the issues in the abstraction such that we don't actually build them in the real system.
Formal methods with Hillel Wayne Said 29 Jul 2026
Concurrency is hard not because human brains cannot handle it but because nobody gets enough practice at it.
I think a large part of the problem of why it's hard for us is because you don't get a lot of practice. Usually when you have a race condition in a system, you find out months later and then you try a fix and you find out weeks later after that if the fix actually worked.
Formal methods with Hillel Wayne Said 29 Jul 2026
Most mathematics will never be useful to a developer; what pays is knowing what mathematics exists so you can find the part that is.
But I think it is more useful for most developers to have an exposure to like what math has in the various fields versus just going all in every single field when they see them, right? You've got to know what's available to know what's most useful for you. And most math will not be useful for you.
Formal methods with Hillel Wayne Said 29 Jul 2026
Programmers fail to recognise how much mathematics their job uses because the mathematics it needs is discrete and school teaches the continuous kind.
And I wonder sometimes if that is the reason people don't recognize the use of math in software engineering is because the math they do need is not the math they've been exposed to.
Formal methods with Hillel Wayne Said 29 Jul 2026
Formal methods shine in highly computational domains and struggle wherever the problem is embedded in human business behaviour.
I think the case of TLA+ and most, not all, but most formal methods, they shine the most in highly computational domains, where most of the problems are highly technical and not like business embedded.
Formal methods with Hillel Wayne Said 29 Jul 2026
Engineers are sceptical of formal methods because they were burned by CASE and UML, sold as miracle solutions and imposed on them regardless of fit.
I think a lot of the reason people are skeptical of these is because they've been burned by things like case and UML and all these other miracle solutions that were forced on them by people who wanted them to use it no matter what.
Formal methods with Hillel Wayne Said 29 Jul 2026
Formal methods are a niche tool; property-based testing is the one most engineers should adopt, and stopping there is a fine place to stop.
I love formal methods, but I think it's a fairly niche tool for most people and I think like property-based testing is in general going to be useful for more people.
Formal methods with Hillel Wayne Said 29 Jul 2026
To get good results out of an LLM you have to already know how to get them without it; the model only makes it faster.
As a general thing we've seen like to get good results you have to already know how to get good results without it. It just helps you get good results faster.
Formal methods with Hillel Wayne Said 29 Jul 2026
AI does a good job of generating a design and still cannot express what the design is supposed to do; that part is the engineer's.
And often I found with my clients I have to tell them like it's doing a good job at generating the actual design, but in actually expressing what the design is supposed to do, it cannot do that yet. You have to do that part yourself.
Formal methods with Hillel Wayne Said 29 Jul 2026
AI is making formal methods more popular without making them mainstream, moving them from about a tenth of a per cent of engineers to three tenths.
I think it is making it more popular. I don't know if it'll make it go mainstream, but it's definitely making it a lot more popular. It's bringing it from maybe like 0.1% to 0.3% which is huge.
Formal methods with Hillel Wayne Said 29 Jul 2026
The software job losses of the past few years were caused more by the end of zero-interest-rate money and the post-COVID crash than by AI.
So, it's hard to tell how much of like the loss of the past few years was AI versus the end of like zero interest rate policy and like the post-COVID crash. And I think it's more the latter, but like again, LLMs are still getting better.
Formal methods with Hillel Wayne Said 29 Jul 2026
Within ten years software development will survive but become ordinary white-collar work, with no more two-hundred-thousand-dollar salaries or unlimited vacation.
I predict that in the next 10 years software development will survive, but it will become like any other white-collar professional work. No more $200,000 salaries, unlimited vacation, or incredible employee bargaining power.
Formal methods with Hillel Wayne Said 29 Jul 2026
Software written for three people, a family or one school, is now possible for everyone, and that will change the world in strange and terrifying as well as exciting ways.
And up until now that like could only really happen if one of those people in that family that community or that school was like really really into computers. But now it's possible for everybody to have situated software.
Formal methods with Hillel Wayne Said 29 Jul 2026
Nobody in software treats debugging as a discipline; it is left as a handful of basic heuristics.
But this is the book that I give to every junior engineer because I think like nobody ever really talks about debugging as like a discipline outside of like basic heuristics.
Formal methods with Hillel Wayne Said 29 Jul 2026
Almost nothing programmers believe is unique to software is actually unique to software.
Almost everything we think is unique about software appears in every other field of engineering.
We Are Not Special Said 20 Jan 2021
Software is not uniquely unpredictable; other engineering disciplines are hit by the same surprises and overruns.
To assume that software is uniquely unpredictable is a special kind of arrogance.
We Are Not Special Said 20 Jan 2021
Software's real advantage over physical engineering is consistency: a component does what it is specified to do every time, while physical materials only fall within a tolerance.
Software is far more consistent than any other kind of engineering.
We Are Not Special Said 20 Jan 2021
The one uncontested difference between software and other engineering is velocity: changing software costs seconds where changing a physical system costs weeks and thousands of dollars.
We can change software much faster than anybody else can change their systems.
We Are Not Special Said 20 Jan 2021
Because software is the cheapest part of a system to change, other disciplines lean on it to paper over their own physical problems, and that reliance has killed people.
Rather than fix a trad issue with trad engineering, Boeing opted for the software kludge, and then people died.
We Are Not Special Said 20 Jan 2021
Software is not less rigorous than traditional engineering; its record-keeping and automated verification are better than most of that field's.
Plenty would kill to get the same kind of automated testing we treat as a given.
We Are Not Special Said 20 Jan 2021
Software's constraints are soft where traditional engineering's are hard, and that is one of the few real differences between them.
But constraints in software tend to be soft constraints.
We Are Not Special Said 20 Jan 2021
Software development is separated from engineering by circumstance rather than essence, and most programmers could cross that gap without retraining.
We are separated from engineering by circumstance, not by essence, and we can choose to bridge that gap at will.
Are We Really Engineers? Said 18 Jan 2021
The argument about whether programming is engineering is conducted entirely by people who have never worked as engineers.
None of the people arguing for or against software engineering as engineering have worked as engineers.
Are We Really Engineers? Said 18 Jan 2021
People who worked as traditional engineers before moving into software say that software engineering is real engineering.
Of the 17 crossovers I talked to, 15 said yes.
Are We Really Engineers? Said 18 Jan 2021
Programming is mathematical work: it uses discrete mathematics rather than the continuous mathematics people picture when they say maths.
Just because we use a different branch of math doesn't mean we're not doing engineering.
Are We Really Engineers? Said 18 Jan 2021
Licensing is a political and social construct, so an unlicensed profession can still be doing engineering.
licenses exist because we are part of society and have legal requirements, not because they are essential to what it means to do engineering
Are We Really Engineers? Said 18 Jan 2021
High consequences cannot be what makes work engineering, because most traditional engineering is low-stakes too.
Much of the engineering there is low-stakes, low-consequence, just like much software is.
Are We Really Engineers? Said 18 Jan 2021
Formal methods are not standard practice even in high-assurance software such as medical devices and aircraft.
most people in high-assurance software don't use formal methods
Why Don't People Use Formal Methods? Said 21 Jan 2019
The hard part of verification is not proving the code correct but working out what the specification should say.
Finding the right spec is one of the biggest challenges in formal methods.
Why Don't People Use Formal Methods? Said 21 Jan 2019
Most distributed-systems outages would have been prevented by slightly more comprehensive ordinary testing, not by better tools.
In fact, the vast majority of distributed systems outages could have been prevented by slightly-more-comprehensive testing.
Why Don't People Use Formal Methods? Said 21 Jan 2019
Full formal verification is a waste of money for most software: near-perfect is reachable with ordinary techniques at a fraction of the cost.
You do not need full code verification to write good software or even to write near-perfect software.
Why Don't People Use Formal Methods? Said 21 Jan 2019
There is a permanent trade-off in verification: an expressive language is hard to prove things about, and a language that is easy to prove things about is hard to write in.
Formal verifiers have a dilemma: the more expressive the language, the harder it is to prove anything in it. But the less expressive the language, the harder it is to write anything in it.
Why Don't People Use Formal Methods? Said 21 Jan 2019
Robert C. Martin's advice makes code worse, because it dismisses every correctness technique that is not unit testing.
Uncle Bob gives terrible advice. Following it will make your code worse.
Uncle Bob and Silver Bullets Said 5 Oct 2017
Programmer discipline is the wrong answer to software defects: the way to reduce them is to change the system so mistakes are harder to make and easier to catch.
Rather, the best way to reduce the volume and severity of mistakes is to adjust the system itself.
Uncle Bob and Silver Bullets Said 5 Oct 2017
Unit tests alone give little confidence in a program, because the mistakes people actually make are not the conveniently unit-testable ones.
But unit tests don't give you much confidence in your code.
Uncle Bob and Silver Bullets Said 5 Oct 2017
What is a korrent?
A korrent is a belief a person has stated in their own words: one sentence stating the claim, backed by a quote and a source, kept at korrents.com.
Under a name here, the quoted block is what they actually said. The korrent beneath it is the claim those words support, in korrents' wording — tap it to see the record, its source, and who else holds it.
Nobody here wrote their own korrents. They are compiled from public statements, and a person can change their mind, which is recorded too.
Recommends rcmnd
rcmnd What they recommend 2 things — each backed by an exact quote.
Compiled by rcmnd.app, not by them: the quotes are theirs, and each links to the post it was copied from.
Recent
Loved Making Software: What Really Works, and Why We Believe It
But no blog post has influenced me as profoundly as Data and Reality or Making Software. There is no blog or talk about debugging as good as the Debugging book.
buttondown.com 6 Aug 2025
What others say about Making Software: What Really Works, and Why We Believe It →
Loved Data and Reality
It's heady and mindbending and delightful and completely changed how I think about software. I love it and recommend it to everybody I meet.
buttondown.com 14 Oct 2019
Where they publish
Blog hillelwayne.com Essays on formal methods, testing and what software correctness costs.
His own domain, where the Crossover Project and most of his writing on TLA+ and verification live.
Recent
- A Crash Course in Predicate Logic 1 Sept 2026 I started writing Logic for Programmers because there weren’t any good resources on logic for, uh, programmers. Now that the book’s out, the new problem is that there aren’t any good free resources on…
- Logic for Programmers is Now Available 29 Jul 2026 I am delighted to announce that my book, Logic for Programmers, is now available! You can check out the release site here or go directly to buy the ebook or print versions. If you bought any of the early access versions…
- Chicago vs New York Pizza is the Wrong Argument 1 Apr 2026 It’s April Cools! It’s like April Fools, except instead of cringe comedy you make genuine content that’s different from what you usually do. For example, last year I talked about The best introductory…
Show 14 more
- Some Silly Z3 Scripts I Wrote 23 Feb 2026 As part of writing Logic for Programmers I produced a lot of “chaff”, code samples and sections I wrote up and then threw away. Sometimes I found a better example for the same topic, sometimes I threw the to…
- A Very Early History of Algebraic Data Types 25 Sept 2025 Been quiet around here! I’ve been putting almost all of my writing time into Logic for Programmers and my whole brain is book-shaped. Trust me, you do not want to read my 2000-word rant on Sphinx post-build LaTeX…
- Gamer Games for Non-Gamers 1 Apr 2025 It’s April Cools! It’s like April Fools, except instead of cringe comedy you make genuine content that’s different from what you usually do. For example, last year I talked about the 3400-year history…
- A Perplexing Javascript Parsing Puzzle 12 Mar 2025 What does this print? x = 1 x --> 0 Think it through, then try it in a browser console! Answer and explanation in the dropdown. Show answer It prints 1. wait wtf At the beginning of a line (and only at the beginning of…
- The Hierarchy of Controls (or how to stop devs from dropping prod) 4 Mar 2025 The other day a mechanical engineer introduced me to the Hierarchy of Controls (HoC), an important concept in workplace safety. 1 (source) To protect people from hazards, system designers should seek to use the most eff…
- Hiatus 11 Sept 2024 All of my budgeted blogwriting time is going to Logic for Programmers. Should be back early 2025. (I’m still writing the weekly newsletter.)
- Toolbox languages 15 Jul 2024 A toolbox language is a programming language that’s good at solving problems without requiring third party packages. My default toolbox languages are Python and shell scripts, which you probably already know about…
- Composing TLA+ Specifications with State Machines 17 Jun 2024 Last year a client asked me to solve a problem: they wanted to be able to compose two large TLA+ specs as part of a larger system. Normally you’re not supposed to do this and instead write one large spec with both…
- What We Know We Don't Know: Empirical Software Engineering 29 May 2024 This version of the talk was given at DDD Europe, 2024. Technology is a multitrillion dollar industry, but we know almost nothing about how it’s best practiced. Empirical Software Engineering, or ESE, is the study…
- Comment Section: Software Friction 14 May 2024 These are some of the responses to Software Friction. Blogs on a similar topic Laurie Tratt wrote What Factors Explain the Nature of Software? which touches on the topic of friction, too. Emails and Comments I’m a…
- Software Friction 1 May 2024 In his book On War, Clausewitz defines friction as the difference between military theory and reality: Thus, then, in strategy everything is very simple, but not on that account very easy. Everything is very simple in w…
- Don't let Alloy facts make your specs a fiction 10 Apr 2024 I’ve recently done a lot of work in Alloy and it’s got me thinking about a common specification pitfall. Everything in the main post applies to all formal specifications, everything in dropdowns is for exper…
- How old is the name 'Daniel'? 1 Apr 2024 It’s April Cools! It’s like April Fools, except instead of cringe comedy you make genuine content that’s different what you usually do. For example, last year I talked about the strangest markets on th…
- Comment Section: The Hunt For The Missing Data Type 18 Mar 2024 I got a lot of responses to The Hunt For the Missing Data Type. I’ve included some of the most interesting ones below. Response Blogs The “missing” graph datatype already exists. It was invented in the…
Link verified 8 Sept 2026. Recent items update automatically from the channel.
Newsletter Computer Things Short pieces on software correctness, more often than the blog.
The shorter, more frequent counterpart to the essays, on the same subjects.
Recent
- NYC, New Webinar, Differential Testing 22 Oct 2026 Been a while! Man, it's so much harder to write essays for a newsletter when I have a full time job writing essays for a company. So three bits of housekeeping first of all: As of last month I now live in NYC! Let me kn…
- What TLA+ can and can't check 30 Sept 2026 Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+1 to find race conditions in code. And now everybody on the internet is talking about formal verification. As a long-time educ…
- The LLMs yearn for the spines 16 Sept 2026 Earlier this year I worked on a couple of AI-generated TLA+ specifications, and one thing I've noticed was that they all used the word "spine" somewhere. Then I saw some non-TLA+ public projects use "spine" too and got…
Show 17 more
- New Post: A Crash Course in Predicate Logic 1 Sept 2026 Logic for Programmers has now been out for a month! To celebrate, I'm releasing the entire second chapter, "A Crash Course in Logic", for free on my blog. Read it here!
- Vim wants you to control, VSCode wants you to consume 18 Aug 2026 Newsletter updates were sporadic in July because of two weddings, two conferences (with two different talks!), and finishing Logic for Programmers. Huge thank you to everybody who bought a copy, as well as for your pati…
- Logic for Programmers is Done 29 Jul 2026 It's done. Logic for Programmers is now 1.0 and available in print. Full announcement here, official website here, direct Amazon link here. If you got an early version of the ebook, you can go back to leanpub to downloa…
- I'm still alive 14 Jul 2026 Between travel obligations and this last heads-down-gotta-get-the-book-done stretch I haven't had time to write any newsletters or even look at social media. The good news is that Logic for Programmers should be done an…
- Logic for Programmers v0.15, Livecoding 17 Jun 2026 There's a new release of Logic for Programmers! This one, version 0.15, is the first true release candidate. There's a couple of minor touch-ups I need to do but all content is in and copy edited and proofread. Unless s…
- Nontrailing separators do not spark joy 10 Jun 2026 This is valid JSON: { "a": 1, "b": 2, "c": 3 } This is invalid JSON: { "a": 1, "b": 2, "c": 3, } The difference is the last comma. The JSON grammar specifies that a comma can separate two members of an object but not po…
- Logic for Programmers extra credits 2 Jun 2026 So I said there wasn’t a proper newsletter this week, since I’m in Budapest prepping for a conference. But I still got a thing for y’all. There’s a lot of interesting topics I wanted to cover for Logic for Programmers,…
- Knowing about things is cheaper than knowing things 28 May 2026 Short one this week because I'm way behind on book and conference prep. Last week a LinkedIn Influencer wrote about how math has nothing to do with programming, so I spite-wrote a rejoinder about how math is necessary t…
- Assumptions weaken properties 20 May 2026 In some tests are stronger than others, I defined STRONG => WEAK to mean "any system passing test STRONG is also guaranteed to pass WEAK". This uses the logical implication operator, defined as P => Q = !P || (P && Q).…
- Points are a weird and inconsistent unit of measure 13 May 2026 I'm in the middle of redoing the Logic for Programmers diagrams and this has surfaced a really annoying problem. The book is formatted in LaTeX using a pseudo-grid of 10.8pt × 7.2pt. The diagrams are done in Inkscape us…
- New Logic for Programmers (and the future of this newsletter) 6 May 2026 So first the immediate news: I just released version 0.14 of Logic for Programmers! This release is pretty similar to 0.13. There are a few rewrites but the vast majority of the changes are layout, copyediting, and tech…
- Illegal vs Unwanted States 28 Apr 2026 An illegal state is a state we never want our system to be in. An unwanted state is a state we don't want to stay in. Many states that we wish were illegal are actually unwanted. Considering a calendaring software which…
- People get confused when language implementations break language guarantees 21 Apr 2026 Take the following Python program: # x = 1, y = 2 x = 0 y = x print([x, y]) It'll print [0, 0]. If we swapped the two assignments, it'd instead print [0, 1]. Each assignment happens in a separate temporal step. Pretty m…
- A sufficiently comprehensive spec is not (necessarily) code 15 Apr 2026 Sorry for missing last week! Was sick and then busy. This week I want to cover a pet peeve of mine, best seen in this comic: A "comprehensive and precise spec" is not necessarily code. A specification corresponds to a s…
- April Cools Post: New York vs Chicago Pizza 1 Apr 2026 Happy April Cools! My not-tech post this year is Chicago vs New York Pizza is the Wrong Argument, which is mostly an excuse for me to talk about Chicago food. See here for all of the other April Cools submissions. As of…
- Choose Boring Technology and Innovative Practices 24 Mar 2026 The famous article Choose Boring Technology lists two problems with using innovative technology: There are too many "unknown unknowns" in a new technology, whereas in boring technology the pitfalls are already well-know…
- LLMs are bad at vibing specifications 10 Mar 2026 No newsletter next week I'll be speaking at InfoQ London. But see below for a book giveaway! LLMs are bad at vibing specifications About a year ago I wrote AI is a gamechanger for TLA+ users, which argued that AI are a…
Link verified 8 Sept 2026. Recent items update automatically from the channel.
GitHub hwayne His TLA+ and formal-methods repositories.
Where the code behind the writing lives, including his TLA+ examples and tooling.
Recent
- learntla-v2 — Learn TLA+ for free! No prior experience necessary! 21 Jul 2026
- lets-prove-leftpad — Proving leftpad correct two-dozen different ways 7 Jul 2026
- tla-pygments — A terrible pygments plugin from a terrible human 18 Mar 2026
Show 10 more
- alloydocs — Proposed documentation for alloytools.org 9 Sept 2025
- tlaplus-exercises — Some experiments in making exercises for teaching TLA+ 7 May 2025
- tla.vim — Vim plugin for TLA+ and PlusCal 3 Feb 2025
- awesome-cold-showers — For when people get too hyped up about things 5 Jan 2024
- autohotkey-scripts — Some of my AutoHotKey scripts 21 Aug 2023
- gpt-tricks — A collection of useful uses of GPT (and other LLMs), organized as examples 18 May 2023
- tla-graphing-demo — A demo of analyzing a TLA+ state graph 7 Apr 2023
- hacker-test-history — Let's explain all the hacker test questions! 2 Aug 2022
- learntla — A TLA+ guide 1 Jul 2022
- sphinx-github-action-test — A quick repo for testing compiling a sphinx doc and syncing it with S3 22 Jun 2022
Link verified 8 Sept 2026. Recent items update automatically from the channel.
About the English under a post
Some people here publish in a language other than English. Where they do, this site shows a machine translation beneath the post, in this typeface — the site's own, not theirs.
The post itself is never changed, moved or hidden: what is set in the serif above is exactly what the person published, and it is what to quote them on. A translation can be wrong in ways that matter, especially about tone.
Only the post's own words are translated. A quoted post, a linked article and a belief on korrents.com are left in their original language.