« | Home | Categories | »

The Coming Software Apocalypse

Posted on September 28th, 2017 at 22:20 by John Sinteur in category: News -- Write a comment


This is why he was so intrigued when, in the appendix of a paper he’d been reading, he came across a strange mixture of math and code – or what looked like code – that described an algorithm in something called “TLA+”. The surprising part was that this description was said to be mathematically precise: An algorithm written in TLA+ could in principle be proven correct. In practice, it allowed you to create a realistic model of your problem and test it not just thoroughly, but exhaustively. This was exactly what he’d been looking for: a language for writing perfect algorithms.

TLA+, which stands for “Temporal Logic of Actions”, is similar in spirit to model-based design: It’s a language for writing down the requirements – TLA+ calls them “specifications” – of computer programs. These specifications can then be completely verified by a computer. That is, before you write any code, you write a concise outline of your program’s logic, along with the constraints you need it to satisfy (say, if you were programming an ATM, a constraint might be that you can never withdraw the same money twice from your checking account). TLA+ then exhaustively checks that your logic does, in fact, satisfy those constraints. If not, it will show you exactly how they could be violated.

  1. Fantastic article. So much more you could say about this… the trade-offs between engineering and hacking, between repeated similar work and novel work, etc. etc.

  2. Anybody have a nice, clean 1961 Ford Falcon for sale? My next car needs to be completely computer free….

previous post: I asked Tinder for my data. It sent me 800 pages of my deepest, darkest secrets

next post: New Rule: The Kremlin Konnection