I would encourage everyone to try this on some self-contained, state-machine like problems, if they have them. At my company, some experts were optimizing our clustering and failover logic by adding a bit more state (and hence complexity). Despite me not being an expert in that area, I was able to find and prevent a catastrophic bug by pointing Opus armed with TLA+ at the problem. It was a bug that was not possible in the prior implementation of the system and no one thought to write unit tests for the sequence of steps that triggers it, so initially went unnoticed. The only thing that caught it was the TLA+ invariants, which, yes, were written by Opus as well.
As a side note, there's a lot of talk about programming being not fulfilling anymore. But the above exercise was probably the most fun I've had with engineering in a long time, and would have been nearly impossible for me personally without AI. Perhaps it was the novelty of the TLA+ stuff, but I think it offers a glimpse into what our jobs could actually be in the future, beyond simply telling Claude to do what you used to do manually and then clicking enter. There are much more ambitious and fulfilling use cases for it.
An UI is a state machine and TLA+ is a tool for validating state machines. You can e.g. ask it to prove that every state is reachable from every other state (so users can’t get stuck somewhere even when a network request fails etc) or you can assert stuff renders correctly in sequence, or that key shortcuts change with the context correctly, or…
I used TLA+ in a (hobby) web app by asking it to model the endpoints and the data user can get from them, and then what kind of access that data can grant in the system, and then implement some properties over that kind of data. I suppose basically like "you can't get access to another user's shopping basket", although mine was maybe a bit more convoluted.
lopatin · · focus · HN ↗
As a side note, there's a lot of talk about programming being not fulfilling anymore. But the above exercise was probably the most fun I've had with engineering in a long time, and would have been nearly impossible for me personally without AI. Perhaps it was the novelty of the TLA+ stuff, but I think it offers a glimpse into what our jobs could actually be in the future, beyond simply telling Claude to do what you used to do manually and then clicking enter. There are much more ambitious and fulfilling use cases for it.
baq · · focus · HN ↗
ndr · · focus · HN ↗
baq · · focus · HN ↗
sn9 · · focus · HN ↗
<a href="https://www.hillelwayne.com/tags/formal-methods/" rel="nofollow">https://www.hillelwayne.com/tags/formal-methods/
_flux · · focus · HN ↗