Are Efficiency and Horizontal Scalability at odds?
Why are scalable systems locally-inefficent, and locally-efficient systems unscalable? Plus, new book release!
What hard thing does your tech make easy?
I occasionally receive emails asking me to look at the writer's new language/library/tool. Sometimes it's in an area I know well, like formal methods. Other...
The Juggler's Curse
It's too cold to go outside, so let's talk juggling.
What are the Rosettas of formal specification?
Plus, new book release!
"Logic for Programmers" Project Update
It'll be done in July.
Formally modeling dreidel, the sequel
2 model 2 dreidel
Stroustrup's Rule
Beginners need explicit syntax, experts want terse syntax.
Hyperproperties
One tier worse than regular properties.
Five Unusual Raku Features
Junctions, whatevers, hypers, and more!
A list of ternary operators
Why let conditionals keep hogging the spotlight?
TLA from first principles
Building an intuition for the mathematics behind the "TLA" in "TLA+"
Be Suspicious of Success
Successful software is buggy software.
How to convince engineers that formal methods is cool
Based on my experiences convincing people it's cool
Refactoring Invariants
Porting a formal methods idea to everyday coding
Goodhart's Law in Software Engineering
It's not just about your boss.
Why Not Comments
Why not "why not" comments? Not why "not comments"
Thoughts on "The Future of TLA+"
What could be added to TLA+ without compromising Lamport's vision?
State and time are the same thing
State is time, time is state.
An idea for teaching formal methods better
Teaching with pseudospecs
Texttools dot py
A small script I find really useful, and you might too!