RSS Parrot

Formally modeling dreidel, the sequel

https://buttondown.com/hillelwayne/archive/formally-modeling-dreidel-the-sequel/

Published: December 18, 2024 16:58

Channukah's next week and that means my favorite pastime, complaining about how Dreidel is a bad game. Last year I formally modeled it in PRISM to prove the game's not fun. But because I limited the model to only a small case, I couldn't prove the game was…

Stroustrop's Rule

https://buttondown.com/hillelwayne/archive/stroustrops-rule/

Published: December 11, 2024 17:32

Just finished two weeks of workshops and am exhausted, so this one will be light. Hanuka Sale Logic for Programmers is on sale until the end of Chanukah! That's Jan 2nd if you're not Jewish. Get it for 40% off here. Stroustrop's Rule I first encountered…

Hyperproperties

https://buttondown.com/hillelwayne/archive/hyperproperties/

Published: November 19, 2024 19:34

I wrote about hyperproperties on my blog four years ago, but now an intriguing client problem got me thinking about them again.1 We're using TLA+ to model a system that starts in state A, and under certain complicated conditions P, transitions to state B.…

Five Unusual Raku Features

https://buttondown.com/hillelwayne/archive/five-unusual-raku-features/

Published: November 12, 2024 20:06

Logic for Programmers is now in Beta! v0.5 marks the official end of alpha! With the new version, all of the content I wanted to put in the book is now present, and all that's left is copyediting, proofreading, and formatting. Which will probably take as…

A list of ternary operators

https://buttondown.com/hillelwayne/archive/a-list-of-ternary-operators/

Published: November 5, 2024 18:40

Sup nerds, I'm back from SREcon! I had a blast, despite knowing nothing about site reliability engineering and being way over my head in half the talks. I'm trying to catch up on The Book and contract work now so I'll do something silly here: ternary…

TLA from first principles

https://buttondown.com/hillelwayne/archive/tla-from-first-principles/

Published: October 22, 2024 17:14

No Newsletter next week I'll be speaking at USENIX SRECon! TLA from first principles I'm working on v0.5 of Logic for Programmers. In the process of revising the "System Modeling" chapter, I stumbled on a great way to explain the temporal logic of actions…

Be Suspicious of Success

https://buttondown.com/hillelwayne/archive/be-suspicious-of-success/

Published: October 16, 2024 15:08

From Leslie Lamport's Specifying Systems: You should be suspicious if [the model checker] does not find a violation of a liveness property... you should also be suspicious if [it] finds no errors when checking safety properties. This is specifically in…

How to convince engineers that formal methods is cool

https://buttondown.com/hillelwayne/archive/how-to-convince-engineers-that-formal-methods-is/

Published: October 8, 2024 16:18

Sorry there was no newsletter last week! I got COVID. Still got it, which is why this one's also short. Logic for Programmers v0.4 Now available! This version adds a chapter on TLA+, significantly expands the constraint solver chapter, and adds a "planner…

Refactoring Invariants

https://buttondown.com/hillelwayne/archive/refactoring-invariants/

Published: September 24, 2024 20:06

(Feeling a little sick so this one will be short.) I'm often asked by clients to review their (usually TLA+) formal specifications. These specs are generally slower and more convoluted than an expert would write. I want to fix them up without changing the…

Goodhart's Law in Software Engineering

https://buttondown.com/hillelwayne/archive/goodharts-law-in-software-engineering/

Published: September 17, 2024 16:33

Blog Hiatus You might have noticed I haven't been updating my website. I haven't even looked at any of my drafts for the past three months. All that time is instead going into Logic for Programmers. I'll get back to the site when that's done or in 2025,…