Wed Mar 17 08:37:48 CET 2010

Mathematical Logic and Compilation

I'm trying to get some intuition straight about specification by
compiler.  I don't find what I'm looking for on the web, so I guess
it's ``obvious'' ;)

In formal mathematics and logic, you have syntax (s) and inference
rules (s1,s2,... -| s) that allow the construction of new syntax.

To alleviate the tedium of working with such a low-level substrate,
one allows the construction of (informal, finitistic) mathematical
structure that talks about manipulation of formula and proofs.
I.e. that talks about the existence of proofs using constructive
methods: algorithms to construct a proof.

Now, in compiler construction one works the other way around:

  * One starts with a physical model (i.e. an electronic circuit).
    This can be abstracted by a mathematical (semantic) model.

  * The objective is then to derive a formal system (syntax and code
    transformation rules) and an interpretation such that the semantic
    model is preserved.

I probably need to look at Model Theory[1] and Proof Theory[2].
( I need to grow some more hair on my chest. )

[1] http://en.wikipedia.org/wiki/Model_theory
[2] http://en.wikipedia.org/wiki/Proof_theory