Also same for all software that requires domain specific knowledge. Which is of course all software. 
me: it is bad that one has to basically become a human SMT solver in order to effectively use these verification tools! I must improve the situation *it gradually becomes apparent that, in order to improve the situation, I too must become a human SMT solver* me: oh no
-
-
-
Yeah, I remember feeling exactly this way about parallelizing compilers not so many years ago
End of conversation
New conversation -
-
-
This is pretty much why I'm glad CSP is a good fit for my problems.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
This should be a “Brah I f’ed my soup” TikTok
-
I am not Online enough to understand this comment
End of conversation
New conversation -
-
-
also a typechecker
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
This discussion is making me think of the “good regulator theorem”
-
“Understanding something sufficiently well is in a precise sense fundamentally the same thing as creating it” is how I understand it (though I don’t understand it very well at all!)
End of conversation
New conversation -
-
-
Invert problem space, normalize, hash or recurse, your call
.Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
In my limited experience, I have learned that (a) it is almost always worthwhile to trust the solver less and write your own specializations and optimizations more, and (b) it is almost always worthwhile to use SMT solvers to discover new optimizations to avoid having to use ...
-
SMT solvers. My superoptimizer has two different "meta-passes" where I use SMT in two different ways to avoid having to test a whole bunch of instruction specializations. Between the two, it's about an order of magnitude speedup.
- Show replies
New conversation -
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.