Ask HN: Do you use TLA+?

49 点作者 riddleronroof超过 3 年前

It's surprising to me that so many crypto projects don't use TLA+. Besides the ones mentioned here (<a href="https://lamport.azurewebsites.net/tla/industrial-use.html" rel="nofollow">https://lamport.azurewebsites.net/tla/industrial-use.html</a>), does your company use TLA+? Why? Why not?

14 条评论

gwd超过 3 年前

Can't speak for crypto projects. I used it to verify some incredibly complicated security fixes I made; you can find my models here:<a href="https://gitlab.com/xen-project/people/gdunlap/tla" rel="nofollow">https://gitlab.com/xen-project/people/gdunlap/tla</a>And the security advisory here:<a href="https://xenbits.xenproject.org/xsa/advisory-299.txt" rel="nofollow">https://xenbits.xenproject.org/xsa/advisory-299.txt</a>A description of the issue, sketches of the attacks, and the fixes can be found in the individual patches.TLA+ was obviously very powerful, but it is incredibly quirky in so many ways. The scoping of variable in PlusCal is really strange: it looks like you can make variables with local scope, but then they turn out to have global scope.You have to fight the tool to be able to use it outside of its special-purpose IDE or make it something that could be sensibly collaborated on over git. (See some of the makefile runes in the above repo to see the kind of thing I did.) Getting it to do parallel searches was difficult.

westurner超过 3 年前

## TLA+Wikipedia: <a href="https://en.wikipedia.org/wiki/TLA%2B" rel="nofollow">https://en.wikipedia.org/wiki/TLA%2B</a>Src: <a href="https://github.com/tlaplus/tlaplus" rel="nofollow">https://github.com/tlaplus/tlaplus</a>Awesome: <a href="https://github.com/tlaplus/awesome-tlaplus" rel="nofollow">https://github.com/tlaplus/awesome-tlaplus</a>### Dr TLA+Web: <a href="https://github.com/tlaplus/DrTLAPlus" rel="nofollow">https://github.com/tlaplus/DrTLAPlus</a>Src: <a href="https://github.com/tlaplus/DrTLAPlus" rel="nofollow">https://github.com/tlaplus/DrTLAPlus</a> :> Dr. TLA+ series - learn an algorithm and protocol, study a specification; [Byzantine] Paxos, Raft, Cosmos,##"Concurrency: The Works of Leslie Lamport" ( <a href="https://g.co/kgs/nx1BaB" rel="nofollow">https://g.co/kgs/nx1BaB</a>##<a href="https://westurner.github.io/hnlog/#comment-27442819" rel="nofollow">https://westurner.github.io/hnlog/#comment-27442819</a> :> Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?

Jtsummers超过 3 年前

To answer "why not?": Because, like a lot of things I've tried to pilot at work, management doesn't see the value when compared against other techniques and the cost of training and maintaining the skillset.I used it on a system to show:1. Where a problem was occurring in a concurrent system's design, and how to fix it by changing the protocol the two processes used to communicate.2. Where a problem was occurring in the data bus of a hardware system. Specifically, which part of the spec had been mis-implemented.Both took as long or longer to do compared to the traditional techniques of hooking up an oscilloscope and looking at results, writing test-specific programs to exercise things, and writing tests to find other problems. It could have been faster if I weren't a TLA+ novice at the time, I think, but then I'd be the only one who understood it. It also wouldn't have been terribly useful for the majority of the time, think 1-2 problems (issues found or new designs) that it may have applied to. I'm willing to work on my own skills outside of work hours (though the last 3 years I've definitely slowed down on that), but the majority of my coworkers aren't (for various reasons, mostly valid, I was single at the time, most of them were married and many had kids, that's a lot of time that's no longer yours). Management isn't willing (mostly the right thing) to spend time and money on training that doesn't have an obvious payback when other techniques work as well (from their perspective) and don't require any extra training or skill maintenance effort.

thamer超过 3 年前

I've used it a few times. It was the most useful either to "prove" the conditions for a bug[1], or to gain confidence that an algorithm I had worked on was safe under tricky conditions involving concurrency.The main downside of TLA+/PlusCal is that it's so different from programming languages that very few engineers are familiar with it. Even PlusCal which is supposed to provide a Pascal-like syntax that gets translated to TLA+ can be tricky to use and has a few pitfalls that can be frustrating for beginners.The tooling is improving, but some design choices are really not ideal. For example, you write PlusCal in a `.tla` file inside a comment block(!) and when you transpile it to TLA+ the generated code is written after your comment, in the same file[2]. This is just one of a number of baffling decisions that create a ton of friction when using these tools. Others on this page have mentioned issues with scope, this is certainly something I've had to fight with.[1] The bug I wrote a model for was CASSANDRA-8287, "Row Level Isolation is violated by read repair": <a href="https://issues.apache.org/jira/browse/CASSANDRA-8287" rel="nofollow">https://issues.apache.org/jira/browse/CASSANDRA-8287</a>. The error trace describes a clear scenario under which this would happen.[2] See this very simple model for an example of how PlusCal is written in a comment block followed by the TLA+ code that's generated from it: <a href="https://gist.github.com/nicolasff/bcc92627485c3d4d9e0c25eeea73b655" rel="nofollow">https://gist.github.com/nicolasff/bcc92627485c3d4d9e0c25eeea...</a>

zerkten超过 3 年前

The "why not" list is long and applies to many niche technologies:* No understanding of formal methods. Even someone is working on a problem that TLA+ would be great at, they don't even know that formal methods exist.* People aren't given time to apply formal methods. Schedules don't allow for getting things correct. It's hard to persuade management to make space for formal methods for various reasons.* Other methods of getting the right (or close to it) product and outcome exist. People are more comfortable with building things and testing them rather than using formal methods. They are willing to take a risk with that approach even if there is a strong argument for formal methods.* People that know/use formal methods tend to gravitate towards niches. Rather than taking on the hard adoption challenges and impacting the culture across large organizations they tend to focus on success niches. Other software engineering mavens are applying arguably easier and less effective processes more successfully across a broad audience.These don't focus on the product itself. TLA+ has challenges as others point out, but it's hard for it to succeed broadly when there isn't a strong desire for the capability. If the user experience got super slick, then there is a chance that it could become such low effort that people would do it, but this doesn't seem a likely outcome.

评论 #30195711 未加载

评论 #30195378 未加载

评论 #30200207 未加载

elcapitan超过 3 年前

I've read Hillel Wayne's "Practical TLA+", which is a very good introduction, and watched a couple of talks on it. I also collect case studies of TLA+ usage. I find the concept really a good idea and would love to use it more.My main issue is that because it's not an everyday tool and has somewhat complex semantics, it becomes hard to use. The syntax and tooling are quite arcane and different from everyday programming languages. That's particularly problematic as it is supposed to be a tool to think about complex issues with it. Translating back and forth between what a spec says syntactically and what it actually means semantically is just hard, and for a non-everyday user, I would expect to make more mistakes when writing a spec or interpreting one I wrote 2 months ago, than I will have with less formal methods that I can actually understand.I wish this was easier and I suspect that having a more mainstream way to express things in TLA+ would get into that direction. I tried to write a toy parser for a language that translates to TLA+, but I didn't get very far yet.

foxfluff超过 3 年前

I've tried it a few times.I wanted to use it a couple days ago to help me understand how a bad state could be reached in a program I was debugging, but found out the tla toolbox no longer starts because it depends on something that's changed in the current java environment (anyone remember write once run anywhere? it was always a lie). I don't have the patience to fight more tools than I absolutely have to.I guess that's my biggest obstacle to using TLA+. I would likely use it if I could just install it from my distro's package manager and have a single clean binary that can be invoked from the command line like a compiler, passing it the path to my model. I find the java gui ux to be repulsive.

nivertech超过 3 年前

What I fail to understand how the same industry which is against "Waterfall"[1]/BDUF[2] is pushing formal methods?There are so many low-hanging fruits to try before using heavyweight formal methods, which will give you a much better ROI:<pre><code> Informal methods: - thinking before coding - writing stuff down - using pen and paper - HDD - Hammock-Driven Development - taking a walk, taking a shower - talking to yourself, talking to people, talking to computer, talking to rubber duck[3] - design reviews Lightweight formal methods: - Decision Tables - Business Rules - FSM and StateCharts - PBT (Property-based Testing) - DbC (Design-by-Contract) - Functional Programming with Algebraic Type Systems - purpose-built problem-specific DSLs - ABM (Agent-based modeling) and simulations </code></pre> --EDIT: Specifically for "Crypto" projects, modeling, simulations, and even Reinforcement Learning probably a better fit than formal specification tools like TLA+/Alloy.It's a huge work to formally specify even a small "smart contract"[4].I don't think that formal specification can model implicit state like the one present in EVM, DApps/JS, and off-chain / out-of-band entities like crypto "Exchanges"[5].Instead of trying to formally specify a "smart contract" written in Turing-complete Solidity and compiled to Forth-like EVM opcodes, it's probably better to write contracts in purpose-built non-Turing-complete financial DSLs with the 1st-class citizen concepts of money, user accounts and transactions.--[1] So called "Waterfall", most people are calling any SDLC with an upfront design phases - "Waterfall", like for example Rational Unified Process (RUP) - which is iterative with overlapping phases.[2] Big Design Up Front[3] RDD - Rubber-duck Debugging[4] which is actually an Agent with a wallet, not a contract in legal or even SW development sense[5] better called unlicensed Broker-Dealers

0xbadcafebee超过 3 年前

Developers are lazy. They don't want to write technical specifications. They can barely be bothered to write a README with the design or make an ADR. They can't even be bothered to write tests half the time.It's also hard to explain to your bosses that you won't have any actual code for 6 months.Experienced lead devs will use it on projects where accuracy and reliability is paramount. Otherwise it's just seen as yak shaving.

评论 #30195716 未加载

评论 #30197597 未加载

评论 #30195407 未加载

codepie超过 3 年前

TLA+ is mentioned a lot here and many people point out how it's practically infeasible to use it in real world systems. Just curious, is there any alternative to write specifications which are more closer to common programming languages and can be used by an average programmer to formally prove correctness?

评论 #30197871 未加载

评论 #30215023 未加载

oauea超过 3 年前

We do use a lot of three letter acronyms, but are trying to curb it because it's confusing for new people.

评论 #30196867 未加载

rchaves超过 3 年前

I think the use of TLA+ is very niche, just to prove that some really lower level algorithms for distributed systems work well, I think crypto might be a good use case like you mentioned, but I guess most companies wouldn’t benefit from it except if for fun

rhinoceraptor超过 3 年前

I would like to, I've been working on learning it in my spare time but it's a big learning curve. It takes a mental shift because it's not programming, it's math.

rchaves超过 3 年前

actually you just gave me an idea where can I apply TLA+ in my job right now, we were thinking hard of many kafka streams and retry mechanisms we need to use, and still guarantee order without being blocking, and I think TLA+ is the perfect tool for the job of checking if we are not missing any edge cases with our current plan

14 条评论

gwd超过 3 年前

westurner超过 3 年前

Jtsummers超过 3 年前

thamer超过 3 年前

zerkten超过 3 年前

评论 #30195711 未加载

评论 #30195378 未加载

评论 #30200207 未加载

elcapitan超过 3 年前

foxfluff超过 3 年前

nivertech超过 3 年前

0xbadcafebee超过 3 年前

评论 #30195716 未加载

评论 #30197597 未加载

评论 #30195407 未加载

codepie超过 3 年前

评论 #30197871 未加载

评论 #30215023 未加载

oauea超过 3 年前

We do use a lot of three letter acronyms, but are trying to curb it because it's confusing for new people.

评论 #30196867 未加载

rchaves超过 3 年前

rhinoceraptor超过 3 年前

I would like to, I've been working on learning it in my spare time but it's a big learning curve. It takes a mental shift because it's not programming, it's math.

rchaves超过 3 年前