Sun Mar 14 15:21:52 CET 2010

Squinting at machine code

Maybe I'm taking the wrong approach trying to capture all this in type

The idea behind Staapl is bottom-up language construction.  Machines
are messy, and with a couple of hacks one can construct a thin layer
on top that has a reasonable, composable semantics.

    Maybe the goal should be: help the assembly programmer?

The whole problem is: there is no exact semantics.  There are
boundaries that are not checked, i.e. stack overflow.

The question is then: how to build something out of this that you can
trust?  How to trust a bunch of rewrite rules from which a semantics
emerges?  How to make the implementation testable?

I.e. given a direct, non-reducing map from stack operations to machine
code.  How do you prove that a reduction produces the same result?
Can we do this statistically?

The main conclusion is that: 

    In the current view it is _not_ feasible to prove the
    transformation rules correct.  They are simply too messy.

    However, by constructing a model of the machine (asm language +
    state) which can accomodate different abstract interpretations,
    and a simpler model of the language it is probably possible to
    make a decent set of tests.