John McCarthy‘s qualification problem[0] relates to this.

While one can and will add invariants, as they are discovered, they cannot all be found.

Entscheidungsproblem and Trakhtenbrot's theorem apply here, counterintuitively that the validity of finite models is in co-re but not in re.

Validity in this case is not dependent by the truth of the premise or the truth of the conclusion.

Basically we have to use tools like systems thinking to construct robust systems, we cannot universally use formal methods across frames.

It is one way race conditions are complex.

Hindsight bias makes it seem easy but that is because that is in the co-re side.

Well intended actions with hindsight can often result in brittle systems as their composition tends to set systems in stone, with the belief that axioms are the end solution.

The fact that Gödels completeness theorem may not apply for finite systems when it works so well for infinite ones is hard for me to remember.

Remembering that axiomatization is a powerful tool but not a silver bullet has actually helped me more than I can count.

[0] http://jmc.stanford.edu/articles/circumscription/circumscrip...

not deleting the active plan seems like a basic fail-safe design choice, and this isn't AWS people's first rodeo. likely there was some rationale for not going with a built-in fallback.

> but it's hardly axiomatic.

Agree, but Time-of-Check to Time-of-Use is a pretty well established failure mode.

Every such analysis will have some hindsight bias. Still, it’s a great post that shows how to model such behavior. And I agree with the another reply that not deleting an active plan seems like a basic fail safe choice which the post also covered

Problem with TLA+ is that it is a completely unrelated tool to the actual programming, and even when everything is done correctly, it doesn't prevent further code changes breaking the model, unless there are work processes in place to update the related model, revalidate it, and only then push the changes into production.

As mentioned previously, I think the only tools that are really valuable should be able to produce code, naturally with multiple possible languages as backends, that are then used as library from the application code.

Something like Lean, F*, Dafny, even if that isn't exactly the same as TLA+.

It’s more than one person at AWS now

Hah, I went to a few of his talks

In my mind, anything that has an actual time period is bound to fail, eventually. Then again, I hang around QA engineers a lot, and when you hear about the selenium troubles of "wait until an element is on the page" stories, you realise it relates to software in general.

QA people deal with problems and edge cases most devs will never deal with. They’re your subject-matter-experts of 'what can go wrong'.

Anyway, the point is. You can’t trust anything "will resolve in time period X" or "if it takes longer than X, timeout". There are so many cases where this is simply not true and should be added to a "myths programmers believe" article if it isn't already there.

"juice wasn't worth the squeeze" - adding that to my vocab

Yeah, I was going to say, if anybody with distributed systems knowledge actually thought about this code, it wouldn't have happened.

If you added model checking to it you could have prevented it though, because people that know how to program a model checking program, will see the error right away.

I don't know if this counts as "research" but this research might be helpful https://www.learntla.com/

I haven't used Alloy (alloytools.org) but it looks interesting and there are good docs. Did you mean "now" instead of "not"?

A lot of people view model checking and similar tools as too theoretical, academic Stuff that can't be so easily applied to the real world.

Here we see the basic steps of modeling a complex system, and how that can be useful for understanding behavior even without knowing the details of every component.