Formal reasoning about states / behavior provides insane leverage for designing products.
It shouldn't be reserved only for expert symbol manipulators.
So @ryanlucas, @wootbeep, and I made an interactive playground + tutorial series: http://sketch.systems .
-
Show this thread
-
For those of us who already know a bunch about formal methods, care to compare this to other tools? To Alloy, to model checkers, to …? What's the underlying state exploration logic?
1 reply 0 retweets 0 likes -
Replying to @ShriramKMurthi @lynaghk and
I enjoyed the traffic light demo, but my "hello world" is a PAIR of [perpendicular] traffic lights, so you can also write basic safety (no two greens) and liveness (eventually each gets green) properties. I'm curious what that looks like.
1 reply 0 retweets 1 like -
Replying to @ShriramKMurthi @lynaghk and
To my understanding this is intentionally just the specification part, not any verification part. It's to make it as easy as possible to communicate with designers and implementers about the spec.
1 reply 0 retweets 1 like -
Replying to @Hillelogram @lynaghk and
But having put all that work into developing a spec, wouldn't you want to do more with it? Put differently, there's a fine line between a "property" (to verify) and a "fact" [as Alloy calls them] (to assert). Would be nice to fluidly move between the two.
2 replies 0 retweets 1 like -
Replying to @ShriramKMurthi @Hillelogram and
http://Sketch.systems is trying to make the very idea of abstract states tangible and compelling to folks who've never been exposed to such thinking. It's trivial compared to Alloy, TLA+, etc. --- no state space enumeration, invariant checking, SAT solver, variable expansion.
1 reply 0 retweets 2 likes -
Replying to @lynaghk @ShriramKMurthi and
People must experience the usefulness of counting with their fingers before they'll be motivated to learn logistic regression. http://Sketch.systems is not for people who already love formal methods; it's for people who've never heard of them.
1 reply 0 retweets 2 likes -
Replying to @lynaghk @Hillelogram and
That seems like an unnecessarily aggressive response, and a bit of a red herring to someone who's thought about these issues a LOT, but thanks for replying and I certainly wish you well.
1 reply 0 retweets 1 like
My apologies --- I was trying to explain our design choices, not make a value judgement or dismiss your question. Our tool doesn't model data or check invariants because *we* don't know how to implement and explain those (useful!) features without compromising accessibility.
-
-
Replying to @lynaghk @Hillelogram and
That's fair. I struggle with those questions too. I hope some day you do figure it out: I worry that without it people will ask whether the effort was worth the payoff. A little magic (like a state explorer) probably goes a long way... Good luck.
0 replies 0 retweets 1 likeThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.