[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)