Perry E. Metzger <perry(a)piermont.com> wrote:
This is a pretty long posting. If you don't care to read it, the TL;DR
is that formal specification and verification is now a real
discipline, which it wasn't in the old days, and there are systems to
do it in, and it's well understood.
Another example, of a somewhat different flavour, is
http://lamport.azurewebsites.net/tla/amazon.html
The difference being that I gather Amazon are using TLA+ more as a
modelling language for distributed systems and not strictly for verifying
implementations.
PS. If there is a historical Lamport / Unix connection, I'm not aware of
one...
Tony.
--
f.anthony.n.finch <dot(a)dotat.at>
http://dotat.at/
protect and enlarge the conditions of liberty and social justice