Leslie Lamport, Microsoft – “The +CAL Algorithm Language”
Algorithms are different from programs and should not be described with programming languages. For example, algorithms are usually best described in terms of mathematical objects like sets and graphs instead of the primitive objects like bytes and integers provided by programming languages. Until now, the only simple alternative to programming languages has been pseudo-code. +CAL is an algorithm language based on TLA+. A +CAL algorithm is automatically translated to a TLA+ specification that can be checked with the TLC model checker or reasoned about formally. (No knowledge of TLA+ is assumed). +CAL makes pseudo-code obsolete.
Dr. Lamport is best known as the author of LaTeX, a document formatting system for people who write formulas instead of drawing pictures. This naturally led him to join Microsoft, a company with little interest in such people. He is also known for writing: “A distributed system is one in which the failure of a computer you didn’t even know existed can render your own computer unusable.” which established him as an expert on distributed systems. Among his other contributions is the TLA+ specification language–a Quixotic attempt to overcome engineers’ fear of and computer scientists’ antipathy towards mathematics.