@buttondown.com.hillelwayne@rss-parrot.net
I'm an automated parrot! I relay a website's RSS feed to the Fediverse. Every time a new post appears in the feed, I toot about it. Follow me to get all new posts in your Mastodon timeline! Brought to you by the RSS Parrot.
---
Hi, I'm Hillel. This is the newsletter version of [my website](https://www.hillelwayne.com). I post all website updates here. I also post weekly content just for the newsletter, on topics like * Formal Methods * Software History and Culture * Fringetech and exotic tooling * The philosophy and theory of software engineering You can see the archive of all public essays [here](https://buttondown.email/hillelwayne/archive/).
Site URL: buttondown.com/hillelwayne
Feed URL: buttondown.com/hillelwayne/rss
Posts: 10
Followers: 2
Solving LinkedIn Queens with SMT
https://buttondown.com/hillelwayne/archive/solving-linkedin-queens-with-smt/
Published: June 12, 2025 15:43
No newsletter next week I’ll be speaking at Systems Distributed. My talk isn't close to done yet, which is why this newsletter is both late and short. Solving LinkedIn Queens in SMT The article Modern SAT solvers: fast, neat and underused claims that SAT…
AI is a gamechanger for TLA+ users
https://buttondown.com/hillelwayne/archive/ai-is-a-gamechanger-for-tla-users/
Published: June 5, 2025 14:59
New Logic for Programmers Release v0.10 is now available! This is a minor release, mostly focused on logic-based refactoring, with new material on set types and testing refactors are correct. See the full release notes at the changelog page. Due to…
What does "Undecidable" mean, anyway
https://buttondown.com/hillelwayne/archive/what-does-undecidable-mean-anyway/
Published: May 28, 2025 19:34
Systems Distributed I'll be speaking at Systems Distributed next month! The talk is brand new and will aim to showcase some of the formal methods mental models that would be useful in mainstream software development. It has added some extra stress on my…
Finding hard 24 puzzles with planner programming
https://buttondown.com/hillelwayne/archive/finding-hard-24-puzzles-with-planner-programming/
Published: May 20, 2025 18:21
Planner programming is a programming technique where you solve problems by providing a goal and actions, and letting the planner find actions that reach the goal. In a previous edition of Logic for Programmers, I demonstrated how this worked by solving the…
Modeling Awkward Social Situations with TLA+
https://buttondown.com/hillelwayne/archive/modeling-awkward-social-situations-with-tla/
Published: May 14, 2025 16:02
You're walking down the street and need to pass someone going the opposite way. You take a step left, but they're thinking the same thing and take a step to their right, aka your left. You're still blocking each other. Then you take a step to the right,…
Write the most clever code you possibly can
https://buttondown.com/hillelwayne/archive/write-the-most-clever-code-you-possibly-can/
Published: May 8, 2025 15:04
I started writing this early last week but Real Life Stuff happened and now you're getting the first-draft late this week. Warning, unedited thoughts ahead! New Logic for Programmers release! v0.9 is out! This is a big release, with a new cover design,…
Requirements change until they don't
https://buttondown.com/hillelwayne/archive/requirements-change-until-they-dont/
Published: April 24, 2025 11:00
Recently I got a question on formal methods1: how does it help to mathematically model systems when the system requirements are constantly changing? It doesn't make sense to spend a lot of time proving a design works, and then deliver the product and find…
The Halting Problem is a terrible example of NP-Harder
https://buttondown.com/hillelwayne/archive/the-halting-problem-is-a-terrible-example-of-np/
Published: April 16, 2025 17:39
Short one this time because I have a lot going on this week. In computation complexity, NP is the class of all decision problems (yes/no) where a potential proof (or "witness") for "yes" can be verified in polynomial time. For example, "does this set of…
Solving a "Layton Puzzle" with Prolog
https://buttondown.com/hillelwayne/archive/a48fce5b-8a05-4302-b620-9b26f057f145/
Published: April 8, 2025 18:34
I have a lot in the works for the this month's Logic for Programmers release. Among other things, I'm completely rewriting the chapter on Logic Programming Languages. I originally showcased the paradigm with puzzle solvers, like eight queens or…
[April Cools] Gaming Games for Non-Gamers
https://buttondown.com/hillelwayne/archive/april-cools-gaming-games-for-non-gamers/
Published: April 1, 2025 16:04
My April Cools is out! Gaming Games for Non-Gamers is a 3,000 word essay on video games worth playing if you've never enjoyed a video game before. Patreon notes here. (April Cools is a project where we write genuine content on non-normal topics. You can…