This looks like a similar approach to TLA+ but, it looks more similar to a markup language that is domain specific. I think that he has a good idea for the mos

This looks like a similar approach to TLA+ but, it looks more similar to a markup language that is domain specific. I think that he has a good idea for the most part and if you did formalize this notation there is a good chance that someone in the computer science domain would eventually program something that could interpret it. Lisp comes to mind.