hwayne

48 ms·

511.
by hwayne 7y ago
Yo, author of PT here. I'd say that given your use case, the book _probably_ won't be that useful to you. Among other things, I intentionally avoided teaching refinements. You'd probably be happier starting with either _Speci
512.
Runway: A tool for distributed systems design(runway.systems)
4 points by hwayne 8y ago|0 comments
513.
by hwayne 8y ago
Speaking as a person who teaches both TLA+ and Alloy, I have a sneaking suspicion that the best way to learn the idea of model checking is _none of the three_. I haven't seriously sat down and deep dived yet, but I'm really liking
514.
by hwayne 8y ago
I really strongly prefer the p-style syntax because it doesn't overload the meaning of `{}`, but a lot of other people in the community use c-style.
515.
by hwayne 8y ago
I'm obviously biased in favor of TLA+, and think it's more useful than people think. But it could also be that another FM might be more useful to you, or that they're not useful at all in your case! Feel free to send me a pin
516.
by hwayne 8y ago
Depends on what you mean by "actual transaction". Every TLA+ behavior is describable as a series of "next-states", where _usually_ (not always, but _usually_) one action is true. In which case you'd model the transa
517.
by hwayne 8y ago
> I think that in computer science in general and formal methods in particular, temporal logic is more well known than all other modal logics combined (and probably more than even the name or concept of modal logic). Man it'd be sup
518.
by hwayne 8y ago
I've seen research tools to extract "real programs" from TLA+. But on the whole not having synthesis as your default case has two major advantages: 1. You can choose the level of modeling, so you can quickly spec out the high
519.
by hwayne 8y ago
A general rule-of-thumb in TLA+ is "default is worst-case". If you don't explicitly declare your actions are fair, they'll be unfair. If you don't explicitly encode atomicity into your spec, it's not atomic. Mu
520.
by hwayne 8y ago
GodDAMN am I behind on updating this There's at least a couple more major improvements I want to make. One is fixing all of the small errors, and one is adding c-syntax. They've been stalled out due to Reasons (tm), but I'm h
521.
by hwayne 8y ago
In my workshops people usually start being able to apply it to their business problems by about day 3. It's actually pretty simple once you get the hang of it! After those two, I'd probably recommend the original _Specifying Syste
522.
by hwayne 8y ago
I've written specifications of Ruby and Python codebases before, and worked with people who wrote Java, C, and Haskell code. It's pretty versatile!
523.
by hwayne 8y ago
In my experience this is how a lot of people practice learning TLA+: taking systems they already know and applying TLA+ to them. The advantage of this is you already know the system pretty well and can use that to check you modeled it corre
524.
by hwayne 8y ago
Alloy forces you to bound all of your models, so it will always terminate.
525.
by hwayne 8y ago
Alloy and Alloy* are used as specification languages, not constraint solvers. There are different speclangs with different specialties, and Alloy is particularly good at domain modeling. Here's an example of an early draft of a spec I&
526.
by hwayne 8y ago
This is a question I lose sleep over. I keep going back and forth on it. Here's my current position: _In my experience_, PlusCal is easier for the average engineer to start with, because it lets me decouple learning about behaviors, le
527.
by hwayne 8y ago
At one point a while back I emailed Stavely to learn more about how it's changed over time, but he's been out of the software world for over a decade now. Of the people I've met who've been on cleanroom projects, the _te
528.
by hwayne 8y ago
<3 You might also like _Software Abstractions_ ( https://mitpress.mit.edu/books/software-abstractions-revised... ), by Daniel Jackson. I read the whole thing in two days and then immediately emailed him gushing about
529.
by hwayne 8y ago
I didn't include it in the article because I wasn't 100% confident in saying so, but I'm reasonably sure that medical devices don't use FM. There's not a whole lot of oversight in that area, and most of the standard
530.
by hwayne 8y ago
I had a section on "high-availability software" that I cut due to not being able to research it thoroughly. For the most part cars and medical devices and stuff don't use FM because there's pretty much no oversight. Airc
531.
by hwayne 8y ago
What, no love for the fox shriek? https://youtu.be/zBpZTo1dlPM?t=26 Also, not as ungodly as the other examples, but I always liked that bald eagles chirped: https://youtu.be/PQ2uMauyBow?t=36
532.
by hwayne 8y ago
Yup, here's some good ones! https://github.com/elastic/elasticsearch-formal-models Along with someone fixing a bug well before someone found the bug in the wild: https://github.com/elastic/ela
533.
by hwayne 8y ago
TLA+ lets you work at much different scales. I have one spec I'm working on where the "domain model" is multiple nodes trying to reach consensus, where some fraction of the nodes are adversarial and intentionally trying to su
534.
by hwayne 8y ago
If it helps at all, I do that a lot too, and have started working on extending my vim plugin[1] to also do configuration and run TLC. Honestly the big blocker here is learning how vimscript better. [1] https://github.com/hwa
535.
by hwayne 8y ago
> It's worth noting that many fuzzers go to great lengths to produce examples that are as small as possible, but it's true that this just comes naturally with TLC. While this is true for invariants, unfortunately it's not
536.
by hwayne 8y ago
One thing I want to caution is that that's the translation of PlusCal to "raw TLA+". If you were not using PlusCal, you might write it a different way. For example, you wouldn't need a `pc` variable because you could exp
537.
by hwayne 8y ago
Nah, different things click with different people. In my experience more beginners find PlusCal easier to start with than "raw" TLA+, which is why I focus on presenting it first. But plenty of people find raw TLA+ more natural to
538.
by hwayne 8y ago
What happens when your Rust has coordinate with an unreliable vendor system written in QBasic? What if a sensor is affected by bad weather? What if there are malicious clients? With specification, we can talk about systems in a wider contex
539.
by hwayne 8y ago
Hey, author here. While right now TLA+ is most popular with cloud and infrastructure companies, that's more because it already has a reputation there than anything. As u/bmays mentioned, at my previous job we were using it to veri
540.
by hwayne 8y ago
That's just testing that all of the test threads are awake after they run once. It only does one buffer operation (the `put` in `synchronized buffer`), and we trivially know it's "broken" if there are only puts and no ge

More ›