Hacker News new | past | comments | ask | show | jobs | submit login

For most programs, you can just use PlusCal instead of straight TLA+ and get most of the benefits. Unless you're writing something that is heavily concurrent or distributed.

I prefer TLA+ (it's both simpler and more powerful than PlusCal), except when specifying something at the code level (e.g. something like weak-memory-model concurrency algorithm).

For 95% of people, PlusCal will suit them just fine.

I'm starting to see people say "I shouldn't learn PlusCal because it's not really TLA+", get disheartened about how difficult TLA+ is to learn, and believe they aren't able to use formal methods. I'd rather 10 people use a slightly-more-limited tool than 1 person use "the real thing".

I don't think TLA+ is "the real thing." I just find it easier. If others find PlusCal easier, then they should definitely start with that.

I have the same opinion about the beauty of TLA+ vs PlusCal, so I find PlusCal frustrating to read. But I don't think the original poster was giving a dismissive opinion of PlusCal. Lamport's genius here is that he made TLA+ accessible via PlusCal. I appreciate this, as well as the video lectures which he made because he "realized that people don't read anymore...".

The video lecture series is amazing and should be mandatory viewing for any CS or SE program IMO.

Applications are open for YC Winter 2020

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact