[TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)

[Tony Finch]

Perry E. Metzger <perry at 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 at dotat.at>  http://dotat.at/
protect and enlarge the conditions of liberty and social justice