Essentially, he seemed to be arguing that, for programs where correctness is very important, we need to think carefully and specify carefully before writing code, and TLA+ is meant to be a tool to do that. He said a team at Amazon has recently had success using it.
Personally, I write executable tests for my code. I see the tests as a specification, which has the huge benefit of proving whether the code conforms to it.
I assume that Mr. Laport, being a brilliant and accomplished computer scientist, has long known about this, and still sees a need for his language. But why?
Are formal specification languages and automated tests complementary approaches, or at odds? Do they lend themselves to different kinds of code?