3 ms·
> 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
by pera 2y ago
> 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?
- ngruhn 2y agoIt's probably just the syntax
- goostavos 2y agoI 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