It’s a mini-blogpost in an Ellie. Written in a “literate programming” style - my comments-to-code ratio has never been so high, I imagine 
7 Likes
Brilliant! And a nice read 
Got it on the second try, you saved my saturday night 
Great post, I have never thought about using test for this purpose! I tried another approach enumerating all possible game states only, and generating all valid paths instead of fuzz testing, but it was harder to develop and too easy to make a mistake because there are 15 states, and obviously in a real case like a webapp this would not be possible in complex cases. But very funny puzzle!
2 Likes
In many quick test implementations this trick is built in.
A lot of them have a forAll function which corresponds to elm test’s fuzz function and corresponds to a ∀ in logic.
They also have an exists function (which doesn’t exist in elm (pun not intended)) and corresponds to an ∃ in logic. It’s implementation follows logic:
∃x.f(x) = !∀x.!f(x)
Which is essentially what OP’s post does.
1 Like
Well, we are not alone:
It seems more common for those that use testing by enumeration (vs random generation), right?
I didn’t immediately follow your post, so let me go at it from a different angle, try to “braindump” what I think is happening in the Ellie and hopefully arrive at the same conclusion 
there doesn't exist a list of Msgs x such that update(x, allLeft) == allRight
!∃x: update(x, allLeft) == allRight
which can be said as
for all lists of Msgs x: update(x, allLeft) /= allRight
∀x: update(x, allLeft) /= allRight
If we extract the update(x, allLeft) == allRight into predicate p(x), then:
!∃x: p(x)
∀x: !p(x)
which are the same. (Cool!)
Alright, so that agrees with your post. I had trouble reading the logic statement, but now I think I can translate it into English for myself:
exists x such that f(x) MEANS THAT not for all x is it true that not f(x)
Exactly.
…