Pesquisa em linguagens de programação e espeficicações formais

Ainda não veio a inspiração (ou foi a preguiça que não deu trégua) para escrever sobre a correspondência de Church-Turing. Enquanto isso, este post, já antigo, de Erik Meijer em seu blog e os comentários discutem muito bem sobre o uso de definições precisas da semântica de uma linguagem de programação. O ponto mais importante, na minha opinião, está nesse parágrafo de Erik:

Of course the question is why smart language designers do not write formal specifications, and why equally brilliant researchers do not cover the complete design of real languages. The simple, recursive, answer I believe is that despite decades of research (van Wijngaarden grammars, attribute grammars, denotational semantics, operational semantics, axiomatic semantics, VDM, ASF/SDF, theorem provers, abstract state machines, ...........................) we still lack the proper programming language to describe real programming languages at the right level of abstraction.

E é ecoado no comentário de Neel Krishnaswami:

Our formal descriptions don't evolve as quickly as our code, for reasons I don't really understand. Eg, SML has evolved much more slowly than Ocaml or Haskell have, AFAICT because it has a formal semantics and they don't. So when a change is made to Ocaml, the implementors don't feel obligated to redo all of the soundness proofs -- which is good, because the proofs are sufficiently unmodular that even small changes can involve lots of work to fix. (Bob Harper and Chris Stone complain about this problem in so many words in their type-theoretic semantics of SML.)