Tricking elm-test into solving a river-crossing puzzle

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 :slight_smile:


Brilliant! And a nice read :+1:
Got it on the second try, you saved my saturday night :sweat_smile:

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.

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 :slight_smile:

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)