Hi Chris, thanks for taking the time to write this, as well as your other paper ("Why Amazon Chose TLA+”). I found the latter through HN. This article answers a lot of questions. Both give me a good context and motivation as I read the TLA HyperBook.