hwayne

33 ms·

481.
by hwayne 7y ago
Feel free to throw an email my way (it's on the website) if you want to chat a bit more about potential use cases.
482.
by hwayne 7y ago
The day after I wrote this, the replication authors came out with their rebuttal rebuttal: http://janvitek.org/var/rebuttal-rebuttal.pdf
483.
by hwayne 7y ago
If you happen to remember some of the pain points, please let me know! I keep a list of the common pitfalls that I need to address in the docs.
484.
by hwayne 7y ago
It's the exact same people, and alloytools.org is now the official site. I agree that it's confusing and let people know that we need a redirect or notice on the old site.
485.
by hwayne 7y ago
Re TLA+, I'll copying my response from the last time Alloy was linked here: --- Alloy comes from the Z line of “systems are basically giant relational algebra problems”, while TLA+ comes from the LTL line of “systems are basically gian
486.
by hwayne 7y ago
There was a fantastic talk at strangeloop this year on Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ . The speaker used it to find a serious security bug in their live code and a feature interaction bug in their UI that
487.
by hwayne 7y ago
Welp, there's my rabbit hole for the week. I've never heard of JOVIAL before, and it looks like there's lot of interesting stuff here. Thank you!
488.
by hwayne 7y ago
> The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you migh
489.
by hwayne 7y ago
I put all of the references, slides, and questions I got here: https://www.hillelwayne.com/talks/what-we-know-we-dont-know/
490.
by hwayne 7y ago
Sometimes the answer is yes, though!
491.
by hwayne 7y ago
Or posing the statements as questions. Like instead of > Myth: People have unique names You write > Do people have unique names? > No, because XYZ. This varies by region because ABC. And in this case, this assumption caused a major
492.
by hwayne 7y ago
For most of the cases where formally verifying _code_ is important, "unit tests" aren't enough. If the person who writes the proofs leaves, you hire someone else to write proofs. Otherwise you don't have a business model
493.
by hwayne 7y ago
It's often really hard to know if an optimization is "correct"- is the same function as the original, unoptimized version. Formal methods helps here by showing they're equivalent, so you can focus on finding good optimiz
494.
by hwayne 7y ago
For 95% of people, PlusCal will suit them just fine. I'm starting to see people say "I shouldn't learn PlusCal because it's not really TLA+", get disheartened about how difficult TLA+ is to learn, and believe they a
495.
by hwayne 7y ago
This is why I usually pitch formal specification as "you build your program faster and spend less time debugging it later." Framing it as a cost-saving measure over a "well ya GOTTA be correct" measure.
496.
by hwayne 7y ago
Not the downvoter, but: - (Bounded) model checking is exhaustive, fuzzing is not. If your system successfully model checks, then no possible input can cause an error. Fuzzing is randomized, so there still _could_ be a bad input. That's
497.
by hwayne 7y ago
It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things like "there are no awful concurrency bugs spanning three servers i
498.
by hwayne 7y ago
This is definitely a possibility! I've interviewed a couple of people and it seems like linked list questions were already traditional by the mid-90's. If "do you remember your formal CS education" was a part of the orig
499.
by hwayne 7y ago
Yeah it absolutely sucks as a measure. You're better off manually counting languages that appear in job postings. That gives you a better breakdown of what people were actually hiring for.
500.
by hwayne 7y ago
Yo, author here. One thing I should really clarify is that while it's a nice sounding argument, my research was pretty haphazard- looking at TIOBE and C programming and extrapolating from there. I recently started doing more thorough r
501.
by hwayne 7y ago
Sadly I don't think it's possible to represent an infinite trace as a SAT problem, so you can't check any liveness properties (will a good thing eventually happen) unless you use something more powerful. Promela/Spin and
502.
by hwayne 7y ago
The big difference between Alloy and mainstream UML is that Alloy can check if your model has properties your want, and if not general a counterexample. A couple use cases for this: 1. You're writing an access control policy feature. T
503.
by hwayne 7y ago
It's worth pointing out that Jackson wasn't specifically thinking of TLA+ when he wrote that. In _Software Abstractions_ he compares Alloy to B, OCL, VDM, and Z. TLA+ is very different from all of those, just as Alloy is. At some
504.
by hwayne 7y ago
There aren't that many public diagrams, so I whipped up a quick example of spec and diagram here: https://gist.github.com/hwayne/2619df2dd7055a57de96f8769c37f... .
505.
by hwayne 7y ago
Alloy comes from the Z line of “systems are basically giant relational algebra problems”, while TLA+ comes from the LTL line of “systems are basically giant temporal logic problems”, which leads to a lot of fundamental differences between t
506.
by hwayne 7y ago
I don't know any game theory so can't say much about the landscape, but I know people've modified PRISM to model games: http://www.prismmodelchecker.org/games/ Fair warning though: PRISM is... weird. You
507.
by hwayne 7y ago
I got the terms from _Software Requirements and Specifications_, which is a fun, if fluffy and meandering, read. I only skimmed the paper you linked but it seems to be a more thorough treatment than the book was. https://www.amaz
508.
by hwayne 7y ago
One of these days I gotta write an in-depth discussion of my teaching logic. The reasons I have for starting with PlusCal are fairly complex, and there are also disadvantages to it, too. But I still think that for many engineers, it's
509.
by hwayne 7y ago
You might be interested in TLAPS, the TLA+ proof system: https://tla.msr-inria.inria.fr/tlaps/content/Home.html There's also this essay on proving TLA+ specifications in Isabelle: https://davecturn
510.
by hwayne 7y ago
In the TicTacToe spec, we have Next2 == /\ turn' = turn + 1 \* A /\ current' = Opponent \* B /\ ∃i,j∈1..N: \* C /\board[i,j] = Empty \

More ›