hwayne

6 ms·

31.
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
32.
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
33.
by hwayne 1y ago
That's not necessarily true. Consider the program `x := 4; loop {if !sum_of_two_primes(x) {return true}; x += 2}`. If we run this on a general purpose CPU, this will halt if and only if Goldbach's conjecture has a counterexample
34.
by hwayne 1y ago
A couple of useful general approaches: - "Metamorphic testing" is where analyze how code changes with changing inputs. For example, adding more filters to a query should return a strict subset of the results, or if a computer visi
35.
by hwayne 1y ago
Oh yeah that's where I remember it from! Pushing an attribution now.
36.
by hwayne 1y ago
I taught a lot of people TLA+ and while there's definitely essential complexity, a nontrivial amount is just syntactic friction. Consider \A x \in set: x.id /= 1 /\ ~x.active vs all x in set: x.id != 1 &&am
37.
by hwayne 1y ago
To be totally fair, my article is about the problem of writing specs when your product features could change week to week, whereas I think u/alfalfasprout is talking about regular updates to an existing system slowly bringing it out of
38.
by hwayne 1y ago
> If you're solving some problem quickly, then we know that what you've solved was not one of the hard problems to begin with. If you're solving some problems in polynomial time, then those problems are in P. I thought com
39.
by hwayne 1y ago
IIRC without that restriction the problem is "just" NP-complete.
40.
by hwayne 1y ago
Proving it's nonpolynomial is pretty easy: just make the goal vector `(10, 10, 10)` and the displacement vectors `{(1, 0, 0), (-10, 1, 0), (-10, -10, 1)}`. It takes ~1000 steps to reach the goal, and if we add one more dimension we nee
41.
by hwayne 1y ago
> Hmm.. I'd love to see a more formal statement of this, because it feels unintuitive. The problem is called "Vector Addition System Reachability", and the proof that it's Ackermann-complete is here: https:/&#x2
42.
by hwayne 1y ago
To be in NP, witness must be verifiable in polynomial time with respect to the size of the original input. In this problem (VAS Reachability), the solution can be `2^2^2^...^K` steps long. Even if that's linear with respect to the witn
43.
by hwayne 1y ago
The `(if -> then; else)` syntax introduces a cut, which I found hides possible solutions.
44.
by hwayne 2y ago
At least in the TLA+ community, the new state-of-art approach is to use the formal model to generate a test suite.
45.
by hwayne 2y ago
I see at least a few errors with the TLA+ code: - It says that `olddb = [k \in Keys |-> CHOOSE v \in Values: TRUE]` initializes olddb nondeterministically. This is NOT true: `CHOOSE` is guaranteed to be a deterministic expression. The ac
46.
by hwayne 2y ago
I couldn't tell you the historical connections, but they "feel" related to me. This comment got me speculating about how to explain this connection; disclaimer I'm writing completely this off the cuff. First off, NFAs an
47.
Fact of Fiction? The Legend of the QWERTY Keyboard(smithsonianmag.com)
1 points by hwayne 2y ago|1 comments
48.
The Curious Case of Quentell(blog.startifact.com)
80 points by hwayne 2y ago|7 comments
49.
Orbit Spirograph (2019)(redblobgames.com)
75 points by hwayne 2y ago|7 comments
50.
by hwayne 2y ago
I think this is unlikely, as the three people involved (Deustch, Lampson, and Thompson) are all American.
51.
by hwayne 2y ago
I thought this was an interesting meditation on the limits of AI and how ordinary people don't see those limits, wrapped up in a context I normally wouldn't expect to see AI at all.
52.
Should we use AI and LLMs for Christian apologetics? (2024)(lukeplant.me.uk)
170 points by hwayne 2y ago|252 comments
53.
Engineer eats efficiently for $2.50 a day (2016)(futureboy.us)
247 points by hwayne 2y ago|442 comments
54.
by hwayne 2y ago
The chapters on both constraint solvers and logic programming are pretty short overviews, we're talking less than 15 pages. I wouldn't recommend it if that's what you're specifically interested in. For SAT/SMT in Py
55.
by hwayne 2y ago
I am amazed that I somehow didn't use the word arity once in the email. That said, I don't believe I'm using the terms unary and binary wrong. "Unary" historically meant "a math operation that takes one para
56.
by hwayne 2y ago
In addition to PlusCal, I think the main "pseudocode alternative" to TLA+ is now Quint: https://github.com/informalsystems/quint
57.
by hwayne 2y ago
The main reason for stuttering is it makes composing specs a lot easier. Say you have two specs, one which is [](x' = x + 1) and one which is [](y' = y + 1). If you put the two together, you get [](x' = x + 1) && [](y
58.
by hwayne 2y ago
You can use the TLA+ spec to generate a test suite: https://arxiv.org/abs/2006.00915
59.
by hwayne 2y ago
I like buttondown because I can directly contact the developer when I have problems. Some downsides to small companies, lots of upsides too.
60.
by hwayne 2y ago
"Compagnies"? Is the secret strategy of big companies "have a lot of typos in your front page?"

More ›