[HN Gopher] Millions of Tiny Databases
       ___________________________________________________________________
        
       Millions of Tiny Databases
        
       Author : feross
       Score  : 105 points
       Date   : 2020-03-04 06:22 UTC (16 hours ago)
        
 (HTM) web link (blog.acolyer.org)
 (TXT) w3m dump (blog.acolyer.org)
        
       | dwohnitmok wrote:
       | Another AWS component with TLA+ use. I'll shill it again because
       | I think TLA+ is one of the most practical formal methods toolkits
       | out there at the moment. It's great. Try it out.
       | 
       | You're not getting rid of implementation bugs with TLA+, but it's
       | a huge breath of fresh air as a formal documentation language.
        
         | mjb wrote:
         | > it's a huge breath of fresh air as a formal documentation
         | language.
         | 
         | Yeah! When I started with TLA+ I was mostly enamored with model
         | checking and proofs. Those turned out to be useful, but the
         | unexpected use of being a really great way to write crisp
         | descriptions of protocols and algorithms is probably a bigger
         | benefit. That's one of the reasons I tend to choose PlusCal
         | over "raw" TLA+ these days: it's easier for others to read and
         | engage with.
         | 
         | After publishing this paper, I had a great email conversation
         | with Leslie Lamport about this use of TLA+. We talked about
         | TLA+'s use as a "low ambiguity documentation" tool, and some of
         | the cases where we've been able to resolve conversations about
         | ambiguities in our implementation because we had the TLA+ spec
         | to fall back on.
        
           | dwohnitmok wrote:
           | Fascinating; did you guys stick almost exclusively to PlusCal
           | (except presumably for writing invariants in TLC)?
           | 
           | I'm quite partial to just using straight TLA+ for everything
           | because it's both what ultimately it all desugars to anyway
           | and because it makes what you put in TLC and what you write
           | for your spec the same language. Plus once you're in the
           | mindset of TLA+, the syntax of PlusCal has always seemed more
           | of a distraction than anything else, but it does seem that
           | PlusCal is a lot less scary for an experienced developer with
           | no TLA+ experience.
        
             | mjb wrote:
             | Speaking only for myself, because we don't have anything
             | approaching a standard here, I do about 60% PlusCal and 40%
             | straight TLA+.
             | 
             | Mostly the tradeoffs are the ones you mentioned. If I was
             | the only audience of what I was writing, I'd pick TLA+
             | every time, but for a broader audience PlusCal can make
             | this stuff much more approachable.
        
               | dwohnitmok wrote:
               | Makes sense. One last question while I still have you
               | here. What's the TLA+ adoption look like within AWS? I
               | imagine it's probably still only a small minority of
               | teams, but exactly how small are we talking (you guys are
               | the only ones, 2-5, 5-10, or 10s?).
        
       | mjb wrote:
       | I'm one of the authors of this paper, along with Fan and Tao. I'm
       | also a huge fan and religious reader of The Morning Paper, so
       | it's really cool to see Adrian feature our work. If you don't
       | know The Morning Paper, be sure to check out some of the other
       | stuff that Adrian writes: deep looks at a mix of systems, ML, and
       | even classic papers.
        
       | webdva wrote:
       | Very inspiring work and achievement. It is perhaps the equivalent
       | of the application of quantum mechanics during the middle to late
       | twentieth century. As such, perhaps "decentralized general
       | computing" is more plausible than I thought.
        
       ___________________________________________________________________
       (page generated 2020-03-04 23:00 UTC)