On 5 January 2013 19:14, Marc Petit-Huguenin <petithug(_at_)acm(_dot_)org>
wrote:
[snip]
Another way to look at it would be to run the following experiment:
1. Someone design a new protocol, something simple but not obvious, and write
in a formal language and keep it secret.
Which raises the obvious question: Why do we not write protocol specs
in a formal specification language instead of struggling with the
ambiguities of natural language?
Theorem provers and automated verification tools could then be brought
to bear on both specifiations and implementations.
Dick
--