Tuesday, April 13, 2010

It's clear that you don't need to fully understand the formal semantics of a language in order to program in it. (There are a lot of languages for which the formal semantics haven't been specified.) How far could you get without knowing the informal semantics?


  1. You can know an informal semantics–but as long as it's informal, you can't be sure that your semantics agrees with the ones used by the compiler writers, or your collaborators. So you get the well-known method of suck-it-and-see. New data, or a compiler upgrade, can unexpectedly reveal differences in behaviour introduced by "optimisations" that you thought were benign–aka bugs.

  2. But then...

    ...if formal semantics is so important, why do we accept incomplete and buggy implementation of the formal semantics

  3. It is a great fallacy to suppose that formalization necessarily improves communication. Both formal and informal semantics are rhetorical strategies by which people attempt to communicate to other people what they have in mind; either may succeed or fail, and what succeeds with one audience may fail with another.

    What is more, speaking of the formal or informal semantics as if it were unique is also misleading. There must be fifty ways to understand C.

    "Almost all theorems are true, but almost all proofs have bugs." —Paul Pedersen, mathematician and hacker

  4. @john,

    Should we agree there is no difference between formal and informal semantics?

  5. I think the real question here is not whether your understanding of the semantics is formal, but whether it's complete. A language lawyer's understanding of semantics covers all possible situations, however unreasonable, but a working programmer's understanding need only cover the situations they encounter in their programs.

    Incomplete understanding isn't necessarily a problem. One can usefully program in Scheme, for instance, without knowing anything about continuations, and one can use continuations for nonlocal exit without understanding their more general power. Since people have very limited intelligence, all of our understanding will be sometimes incomplete, and language semantics is not a particularly dangerous place for that incompleteness. When it becomes a problem, we can learn more.

    Compilers, of course, don't have that option, so their understanding must be close to complete, although it needn't match the formal semantics in all cases — users will accept limitations like finite memory, and sometimes even semantic holes like Schemes without reusable continuations or tail-call optimization.