Ron Pressler's blog
Visit pron.github.io → RSS feedOn Hacker News May 2017 – Jun 2017
We learn how to encapsulate and compose TLA+ specifications, of the precise mathematical definition of abstraction, and compare TLA+'s notion of abstraction with those of other formalisms. Plus some various cool stuff.
TLA, the Temporal Logic of Actions is the core of TLA+. It is a temporal logic that minimizes the use of temporal reasoning in favor of more ordinary mathematics. It is a general mathematical framework for describing and reasoning about algorithms and systems.
TLA+ is a formal specification and verification language intended to help engineers specify, design and reason about complex, real-life algorithms and software or hardware systems. We explore its motivation, application and principles of design.