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.