On May 30rd, I started the #100DaysOfCode challenge to learn more about formal methods and see how much we could use them in our daily software tasks. 100 days of code: Day 0 of learning TLA+ for regular software development will give you the introduction into this journey.

As with my regular notes, I’ll share the surprising or thought-provoking discoveries I make.

Since the LearnTLA website by Hillel Wayne seems to be the reference, I started here. And the website is indeed great for a step by step introduction!

Today’s mind twisting moment came from this part of the expression explorations

CASE TRUE -> FALSE
  [] TRUE -> TRUE

If more than one match, though, TLC will pick one for you and not branch. In other words, the following code May or may not be true. Be careful

This took me a few seconds to digest.

Then it start to make sense. I already got that the model checker explores the various state spaces, and so that we need to think in states and not in steps. Form this, yes it makes sense, since the case do not explore all the states like a in would do, then any state would match.

For instance,

l = []
x in ["a", "b", "c"]
    l = append(l, x)
    print l

Will print

["a"]
["b"]
["c"]

3 different state paths, no 3 sequential steps.

It starts to sink in.

Wish me luck, it’s only the beginning of the journey ;)

If you liked this, you can find the other posts of my #100 days of code: formal methods

If you’re interested in this, keep an eye on my notes in the next weeks. If you follow me on Twitter, I’ll also share the updates there.