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