←back to thread

Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods

(queue.acm.org)
167 points yarapavan | 2 comments | 01 Apr 25 14:59 UTC | HN request time: 0.423s | source
Show context
pera ◴[01 Apr 25 16:32 UTC] No.43548743[source]▶
> we also sought a language that would allow us to model check (and later prove) key aspects of systems designs while being more approachable to programmers.

I find it a bit surprising that TLA+ with PlusCal can be challenging to learn for your average software engineer, could anyone with experience in P show an example of something that can be difficult to express in TLA+ which is significantly easier in P?

replies(1): >>43556743 #
1. ngruhn ◴[02 Apr 25 13:55 UTC] No.43556743[source]▶
It's probably just the syntax
replies(1): >>43559486 #
2. goostavos ◴[02 Apr 25 18:05 UTC] No.43559486[source]▶
I think it goes beyond that.

TLA+ requires you to think about problems very differently. It is very much not programming.

It took me a long time (and many false starts) to be able to think in TLA. To quote Lamport, the real challenge of TLA+ is learning to think abstractly.

To that, I think plusCal and the teaching materials around it do a disservice to TLA. The familiar syntax hides the wildly different semantics