Hi all,
the main use of TLAPLUS is for specifying algorithms from beginning
but I have found it very useful to understand some parts of a standard.
Understanding in the details the usual arithmetic conversion function designed by the C99 standard
(p. 45) can be challenging because of its intermingled use of ranks, types, domains, promotion...
http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf
For instance using TLAPLUS to give precise and short definitions of the many types categories (p. 33)
(standard signed types, complex types; extended signed integer types and so on and so forth)
helps understand the whole system.
It also helps understand that many parts of the standard are not as clear as they should be.
In his 1902's letter to Frege, Russel wrote "The exact treatment of logic in fundamental questions,
where symbols fail, has remained very much behind [...]" I think the same sentence
can be applied to standards: "The exact treatment of standards in fundamental questions,
where symbols fail, has remained very much behind [...]"
http://isites.harvard.edu/fs/docs/icb.topic1219929.files/FregeRussellCorr.pdf
--
FL