Archive • Computer Things • Buttondown

Hyperproperties

November 19, 2024

One tier worse than regular properties.

Five Unusual Raku Features

November 12, 2024

Junctions, whatevers, hypers, and more!

A list of ternary operators

November 5, 2024

Why let conditionals keep hogging the spotlight?

TLA from first principles

October 22, 2024

Building an intuition for the mathematics behind the "TLA" in "TLA+"

Be Suspicious of Success

October 16, 2024

Successful software is buggy software.

How to convince engineers that formal methods is cool

October 8, 2024

Based on my experiences convincing people it's cool

Refactoring Invariants

September 24, 2024

Porting a formal methods idea to everyday coding

Goodhart's Law in Software Engineering

September 17, 2024

It's not just about your boss.

Why Not Comments

September 10, 2024

Why not "why not" comments? Not why "not comments"

Thoughts on "The Future of TLA+"

September 4, 2024

What could be added to TLA+ without compromising Lamport's vision?

State and time are the same thing

August 27, 2024

State is time, time is state.

An idea for teaching formal methods better

August 21, 2024

Teaching with pseudospecs

Texttools dot py

August 14, 2024

A small script I find really useful, and you might too!

Why I prefer rST to markdown

I will never stop dying on this hill

My patented Miracle Tonic would have prevented the CrowdStrike meltdown

𝄞 Try Hilleli's 𝅘𝅥𝅮 Miracle Elixir 𝅘𝅥

Keep perfecting your config

Make your tools work better for you.

Logic for Programmers now in early access!

I am delighted to announce that Logic for Programmers is now available for purchase! While still in early access, it's almost 20,000 words, has 30 exercises,...

Solving a math problem with planner programming

More opportunities to mess with exotic technology

A brief introduction to interval arithmetic

Why x^2 isn't always x*x.

Logic for Programmers Update

I spent the early week recovering and the later week working on Logic for Programmers ([init] [update]) because I have a self-imposed deadline of mid-July,...

New blog post: Composing TLA+ Specifications

Post here! It's a really advanced TLA+ technique that I'm sure will alienate 90% of my readers. Patreon here. Anyway, I'm off to get a bone graft. Proper...

Nondeterminism in Formal Specification

Just an unordered collections of thoughts on this. In programming languages, nondeterminism tends to come from randomness, concurrency, or external forces...

I've been thinking about tradeoffs all wrong

It's not about what's better, it's about what's less worse.

NoCode Will Not Bring Computing to the Masses

NoCode, scripting vs applications, and software marketplaces

What I look for in empirical software papers

Oh God it's already Thursday

Paradigms succeed when you can strip them for parts

On the value of "scavenging" for paradigm adoption

"Integration tests" are just vibes

New blog post, and some thoughts on what makes an integration test an "integration" test.

"Testing can show the presence of bugs but not the absence"

An analysis of the ramifications.

What makes concurrency so hard?

Is it something about human brains, or something about the problem domain?

Some notes on for loops

Experts can learn a lot by looking at the basics.

Why do regexes use `$` and `^` as line anchors?

A history that will satisfy nobody.

What if the spec doesn't match the code?

Address people's biggest concern about formal methods

What Mob Programming is Bad At

Bulldozers vs Lightning Bolts

How to argue for something without any scientific evidence

It's all about the show

Know (of) the right tool for the job

February 27, 2024

Plus: Using LLMs for data queries

Planning vs Model Checking

February 20, 2024

Comparing two software technologies you've probably never heard of

Strings do too many things

February 8, 2024

The most powerful and terrible of all basis types

What does 'TLA+' mean, anyway

January 30, 2024

The secret Illuminati meaning behind the Three Letter Acronym (plus)

GitHub Search for research and learning

January 24, 2024

Also, new blog post!

Unusual basis types in programming languages

January 17, 2024

All languages have numbers, booleans, strings, and lists. What else is out there?

Why all([]) is true, prod([]) is 1, etc

January 9, 2024

It's all monoids! Monoids for everyone!

Advice for new software devs who've read all those other advice essays

December 19, 2023

From a person who really shouldn't be giving others advice.

I formally modeled Dreidel for no good reason

December 12, 2023

I can mathematically prove the game's not fun.

When would you ever want bubblesort?

December 4, 2023

There are very few universal rules in software engineering, but there are are a lot of near-universal principles. Things like "prefer composition to...

How do you take the average of two timestamps?

November 9, 2023

A jaunt through affine measures and math loopholes

Some thoughts on software expertise

November 7, 2023

(Note, there's some important administrative stuff after the newsletter.) I think a lot about the nature of expertise. While I write about all sorts of...

I shouldn't be so harsh on teaching TLA+ with puzzles

November 2, 2023

I know I'm getting the newsletter out very late this week (this kind of lackadaisical nonprofessionalism is why I don't offer paid subscriptions) so I'll...

Raku is surprisingly good for CLIs

October 26, 2023

A while back I wrote Raku: a Language for Gremlins about my first experiences with the language. After three more months of using it I've found that it's...

I wish people would do historical arguments better

October 24, 2023

Just because the historical context for a practice was different doesn't mean it's useless in the current context

Some thoughts on good spec properties

October 10, 2023

Lots of updates this week! First of all, my talk Is Software Engineering Real Engineering is now available online! It's the video version of the crossover...