hwayne

11 ms·

1.
by hwayne 7mo ago
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 has a reference to a value, that value
2.
by hwayne 7mo ago
...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.
3.
by hwayne 8mo ago
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 "field notes" repo from a
4.
by hwayne 8mo ago
Check out datalog! https://learn-some.com/ The tutorial there uses Clojure syntax but Datalog normally uses a Prolog syntax.
5.
by hwayne 9mo ago
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 world can do more than the machine, and the proper
6.
by hwayne 9mo ago
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 eventually look the same for all open browser tabs on th
7.
by hwayne 9mo ago
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 think you could show an AP calculus studen
8.
by hwayne 9mo ago
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 needed to take the mean of a sequence.
9.
by hwayne 9mo ago
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, so maybe that's asking too much
10.
by hwayne 9mo ago
> 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 areas, though. I think it's disingenuous to say that TL
11.
by hwayne 9mo ago
Thanks for sharing the general term! I didn't know about it.
12.
by hwayne 11mo ago
Now you just gotta go to the first submission and post a link here. Complete the circle!
13.
by hwayne 11mo ago
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 "disjoint union" and "direct s
14.
by hwayne 1y ago
I love how you create dataclasses to abstract over constraints!
15.
by hwayne 1y ago
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
16.
by hwayne 1y ago
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. Satisfaction problems, like finding counterexamples in rulese
17.
by hwayne 1y ago
Now I'm mad I didn't remember the word "antics". It's so much more evocative than "crimes"!
18.
by hwayne 1y ago
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 moon in deep ditch in earth's bottom and will eat up sta
19.
Motif-Index of Folk-Literature (1958) [pdf](ia600301.us.archive.org)
6 points by hwayne 1y ago|1 comments
20.
by hwayne 1y ago
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-txns-modular-v...
21.
by hwayne 1y ago
If you put the spec online I'd be happy to give it a quick optimization skim!
22.
by hwayne 1y ago
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 directly for now.
23.
by hwayne 1y ago
I remember you showing me this! Wow that was a long time ago.
24.
by hwayne 1y 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 Art of All Time if it was.
25.
Best Illusion of the Year 2023 Winners(illusionoftheyear.com)
1 points by hwayne 1y ago|1 comments
26.
by hwayne 1y ago
I think of the two P-lang probably has a brighter future. I don't know how many people are working on Spin besides Holzmann, while P has a lot of institutional support and development budget at AWS.
27.
by hwayne 1y ago
Right now the best practice is generating test suites from the TLA+ spec, though right now it's bespoke for each company that does it and there's no production-ready universal tools do that. LLMs help.
28.
by hwayne 1y ago
With one client I have, we know the TLA+ model is accurate because we're extracting tests directly from the spec. It's kind of a riff on what MongoDB does in this paper: https://arxiv.org/abs/2006.00915
29.
by hwayne 1y ago
This is a quick demo of TLA+ I like: https://gist.github.com/hwayne/39782de71f14dc9addb75f3bec515... It models N threads non-atomically incrementing a shared counter, with the property "the counter eventually equa
30.
by hwayne 1y ago
`S = {str -> bool}` is actually uncountable. `S` is isomorphic to the power set (set of all subsets) of `str`, and `2^str` is at least as big as the set of real numbers, as any real number (like π) can be mapped to the set of string pr

More ›