Viewing profile — hwayne

The key bit is that specifications don't need to be "obviously computable", so they can be a lot simpler than the code that implements them. Consider the property "if some function…

...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.

I'll warn you that Picat is very much a "research language" and a lot of the affordances you'd expect with a polished PL just aren't there yet. There's also this really great "fiel…

Check out datalog! https://learn-some.com/ The tutorial there uses Clojure syntax but Datalog normally uses a Prolog syntax.

Also: - Have a clear notion of what part of the specs represents the system under your control (the "machine"), and what part represents the broader world it interacts with. The wo…

I've had to help a client with something not exactly like, but with similar properties as, Google Docs. One of the big properties they had to engineer in was "the doc should eventu…

I think the "high school math" slogan is untrue and ultimately scares people away from TLA+, by making it sound like it's their fault for not understanding a tough tool. I don't th…

Those things, unlike floats, have approximable-enough facsimiles that you can verify instead. No tools support even fixed point decimals. This has burned me before when I e.g neede…

I really do wish that PRISM can one day add some quality of life features like "strings" and "functions" (Then again, AIUI it's basically a thin wrapper over stochastic matrices, s…

> No problem with floats or strings as far as specification goes. The particular verification tools you choose to run on your TLA+ spec may or may not have limitations in these are…

Thanks for sharing the general term! I didn't know about it.

Now you just gotta go to the first submission and post a link here. Complete the circle!

Since writing this I've been informed of some gaps (mostly through email and a lobsters [1] thread). Some of the main ones: - McCarthy's "Direct Union" is probably conflating "disj…

I love how you create dataclasses to abstract over constraints!

Even worse than that, SMT can encode things like Goldbach's conjecture: from z3 import \* a, b, c = Ints('a b c') x, y = Ints('x y') s = Solver() s.add(a > 5) s.add(a % 2 == 0) the…

It really depends on the kind of solving you want to do. Mathematical optimization, as in finding the cheapest/smallest/whatever solution that fits a problem? OR-Tools. Satisfactio…

Now I'm mad I didn't remember the word "antics". It's so much more evocative than "crimes"!

Entertaining collection of Folklore classifications. Some examples: - T550.6. T550.6. Only half a son is born by queen who ate merely half of mango. - A1066. A1066. Sun will lock m…

Main way we're validating that now is by using TLA+ models to generate test suites. Mongo came out with a new paper on this recently: https://will62794.github.io/assets/papers/mdb-…

If you put the spec online I'd be happy to give it a quick optimization skim!

Apparently they're getting very good: https://emschwartz.me/new-life-hack-using-llms-to-generate-c... I try not to use them too much because I want to build the skill of using SMTs…

I remember you showing me this! Wow that was a long time ago.

My favorite is the third place, "Cornelia". Mostly because I feel like it's something that could have been made in the Renaissance and would have been considered among the Greatest…