On Thu, Oct 13, 2016 at 3:54 PM Konstantin Khomoutov <
> That's because there's the difference between the so-called normative
> texts and so-called informative texts. Normative texts intently use dry
> language with as minimal wording as possible to not accidently state
> more than should have stated. You can found this pattern everywhere --
> from civil laws to patents to RFCs and ITU-T recommendations etc.
An even better approach is to write the text in a formal semantics such as
structural operational semantics. This removes another layer of
interpretative error in the text. It has been done for real-world
languages: Standard ML is an example, where its 1997 specification is about
very close to the ideal as well.
One powerful aspect is that you can then write every rule from the
semantics into, say, a Prolog system and then you can ask the system what
the correct behavior is for a given program. This allows multiple
implementations to solve discrepancies by asking the spec who is right.
One caveat though is that in the last couple of years much have happened in
the area. You would not write a modern spec as is done in the 1997 SML
spec, as we have learnt that there are some constructions which look
formal, but aren't. That is, even if your goal is formality, there are
informal assumptions you have made which in turn gives a window for
interpretation. A long term goal is to eliminate those.
You received this message because you are subscribed to the Google Groups
To unsubscribe from this group and stop receiving emails from it, send an email
For more options, visit https://groups.google.com/d/optout.