[HN Gopher] A walkthrough tutorial of TLA+ and its tools: analyz... ___________________________________________________________________ A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue Author : pron Score : 43 points Date : 2020-03-05 18:13 UTC (4 hours ago) (HTM) web link (github.com) (TXT) w3m dump (github.com) | pron wrote: | This is the coolest demonstration of TLA+ I've seen to date. It | takes you through specification, implementation, model-checking | with TLC, visualization and animation, checking an inductive | invariant, deductive proofs mechanically checked by TLAPS, | refinement mapping and even model-based trace checking. | fizwhiz wrote: | OT: I don't know if this level of rigor is employed by any | major libraries. I know AWS has used it a great deal for their | systems though notably recently[1] | | [1] | https://assets.amazon.science/c4/11/de2606884b63bf4d95190a3c... | kureikain wrote: | If anyone is trying to learn TLA+, this site looks like a good | one: https://learntla.com/ too ___________________________________________________________________ (page generated 2020-03-05 23:00 UTC)