by riddleronroof on 2/3/22, 3:13 PM with 24 comments
by gwd on 2/3/22, 5:11 PM
https://gitlab.com/xen-project/people/gdunlap/tla
And the security advisory here:
https://xenbits.xenproject.org/xsa/advisory-299.txt
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.
by westurner on 2/3/22, 4:59 PM
Wikipedia: https://en.wikipedia.org/wiki/TLA%2B
Src: https://github.com/tlaplus/tlaplus
Awesome: https://github.com/tlaplus/awesome-tlaplus
### Dr TLA+
Web: https://github.com/tlaplus/DrTLAPlus
Src: https://github.com/tlaplus/DrTLAPlus :
> Dr. TLA+ series - learn an algorithm and protocol, study a specification; [Byzantine] Paxos, Raft, Cosmos,
##
"Concurrency: The Works of Leslie Lamport" ( https://g.co/kgs/nx1BaB
##
https://westurner.github.io/hnlog/#comment-27442819 :
> Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?
by Jtsummers on 2/3/22, 4:59 PM
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.
by thamer on 2/3/22, 6:08 PM
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": https://issues.apache.org/jira/browse/CASSANDRA-8287. 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: https://gist.github.com/nicolasff/bcc92627485c3d4d9e0c25eeea...
by zerkten on 2/3/22, 5:16 PM
* 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.
by elcapitan on 2/4/22, 9:55 AM
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.
by foxfluff on 2/3/22, 5:06 PM
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.
by nivertech on 2/3/22, 11:21 PM
There are so many low-hanging fruits to try before using heavyweight formal methods, which will give you a much better ROI:
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
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
by 0xbadcafebee on 2/3/22, 5:03 PM
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.
by codepie on 2/3/22, 6:46 PM
by oauea on 2/3/22, 4:41 PM
by rchaves on 2/3/22, 4:40 PM
by rhinoceraptor on 2/3/22, 6:25 PM
by rchaves on 2/3/22, 8:09 PM