> If it were a technical journal, maybe they wouldn't be related. But they're definitely related for a popular article. Hence my last paragraph -- they're only

> If it were a technical journal, maybe they wouldn't be related. But they're definitely related for a popular article. Hence my last paragraph -- they're only related in the sense that the entire formal methods/verification/theorem proving community is related. Given the hundreds of systems/researchers that would make for interesting additions to the story, it's not surprising that TLA+ isn't mentioned. (Incidentally, the author's choice representative for "other people are doing this too" -- Automath -- is probably just as good of a choice as TLA+.)