hwayne

22 ms·

361.
by hwayne 5y ago
> What does Bertrand Meyer have to do with the history of UML? Good question! While he wasn't involved with the standardization of it, he was one of the first major opponents, primarily because 1) was already a giant in OOP methodol
362.
by hwayne 5y ago
UML statecharts are based on the theory of Harel statecharts, which you might find interesting: http://www.inf.ed.ac.uk/teaching/courses/seoc/2005_2006/reso...
363.
by hwayne 6y ago
As also mentioned on Twitter, I think I'm taking the criticism of this article much harder than usual. I have a response to your comment, but it's a bit "sideways" from the actual discussion. Ping me on email/twitte
364.
by hwayne 6y ago
Would you be willing to provide a full example, replicating the dependent spec?
365.
by hwayne 6y ago
If I'm being honest, a comment from /u/neel_k on this is enough to make me doubt my entire premise. He's a giant in the field and knows many, many things I don't.
366.
by hwayne 6y ago
I used LTL because it's simple enough to explain the core ideas without getting bogged down in affordances and details. It's purely a pedagogical choice, just like how nobody explains the halting problem in terms of Java. Switchin
367.
by hwayne 6y ago
Then you've left the realm of formal specification of systems, though, so you're entirely outside the scope of the problem.
368.
by hwayne 6y ago
Clojure Spec is a contract system, which is a common way to write code specifications. You can formally verify it in theory; ACL2, another lisp, is used in formal verification. It's also hard to compose formally-verified code, as Lars
369.
Baking a Hello World Cake(mike-worth.com)
1 points by hwayne 6y ago|0 comments
370.
TLA+ Graph Explorer(github.com)
103 points by hwayne 6y ago|6 comments
371.
Every Noise at Once(everynoise.com)
344 points by hwayne 6y ago|94 comments
372.
by hwayne 6y ago
One of the reasons I'm so bullish on TLA+ is that "the tooling has some issues" is a fixable problem, and the bigger the community, the more likely it is to get fixed.
373.
by hwayne 6y ago
The other one I know about is PGo, which is a bidirectional go-pluscal compiler: https://github.com/UBC-NSS/pgo
374.
by hwayne 6y ago
I've never used salt myself so couldn't tell you. From a skim, it looks like they don't have module instantiation? Depending on what you're doing that could be a limitation.
375.
by hwayne 6y ago
It's still a barrier for beginners. I teach both TLA+ and Alloy and people struggle with remembering TLA+ tokens much more than they do with Alloy, which has synonyms for common operators. You can write `implies` instead of `=>` if
376.
by hwayne 6y ago
The syntax isn't for everyone and the tooling has some issues.
377.
by hwayne 6y ago
This messes me up when I'm writing actual LaTeX because I keep writing `\A` instead of `\forall` EDIT: Also that spec uses a lot of really interesting techniques, such that doing a breakdown would be a good Blub study. Off to the typew
378.
by hwayne 6y ago
It's worth noting that while it's not anything special from a math point of view, there's a lot more technique involved in specifying and verifying `ImplSpec => AbSpec`, which is why it's considered a more advanced to
379.
by hwayne 6y ago
We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt
380.
by hwayne 6y ago
(3) is backwards: it's a prediction, not a deduction. I had the theory "LL questions were meant to test C/Pascal knowledge", based on studying `net.jobs`. I then came up with a test for the theory: if it was true, then t
381.
by hwayne 6y ago
Yep! Probably not immediately (this post was a writeup of research I did in 2019), but it'll happen. I also want to dive Byte Magazine archives to see if they have anything interesting to say, too.
382.
by hwayne 6y ago
Author here. Why wouldn't interviewing DMs on Twitter be research? I'm getting "oral histories" from a bunch of different people and comparing them for common patterns. It wasn't the only thread of research I did, b
383.
by hwayne 6y ago
Just to head off any speculation about the reasons I didn't study CS books, it's 100% because I Just Forgot > While reviewing this post, my friend Alex Koppel suggested another idea: comparing how much the corresponding languag
384.
by hwayne 6y ago
If you don't have any concurrency or nondeterminism in your spec, then you'll probably want different tools. It's not that TLA+ is bad at modeling single-threaded algorithms, it's just that makes a lot of design decisi
385.
by hwayne 6y ago
Fun fact: Emina Torlak also wrote Kodkod, the constraint solver used to convert Alloy specs into SAT problems. She's pretty cool!
386.
by hwayne 6y ago
I think you'd be better off starting with a simpler formalism for this, like Linear Temporal Logic. That's a good pick because there's a straightforward mapping to Büchi automata. This will give you some more intuition on mod
387.
by hwayne 6y ago
I use a personal wrapper around the command line for most of my work. It's incomplete and has a few holes, but it gets the job done for me. https://github.com/hwayne/tlacli
388.
by hwayne 6y ago
Heckin'! One of my favorite things to see in TLA+ adoption is people making more tools to work with it.
389.
by hwayne 6y ago
> 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbit
390.
Skycircles: What's Flying Above Us?(skycircl.es)
2 points by hwayne 6y ago|0 comments

More ›