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

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!

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.

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

notfor all x is it true thatnotf(x)

Exactly.

…