UampirNexol

UampirNexol is a proof-of-concept implementation of Machine State Combinators. To quote that article:

We are interested here, not in designing a high-level language with good code-structuring facilities that compiles to a given machine language, but in designing a low-level language, hardly distinguishable from a given machine language, that nevertheless has good code-structuring facilities.

It is a language in which MOS 6502 machine language programs can be expressed as functions which map machine states to machine states. These functions are used as combinators which are composed in the manner of Function-level programming. Once a complete program is constructed from these functions, 6502 machine code can then be extracted that can be executed on a 6502-based computer.

For a fuller description of the language, see the file doc/Definition-of-UampirNexol.md, which gives a definition of the language as a literate test suite written in Falderal.

Quick start

• Install ghc. (tested with versions 8.8.4 and 9.2.8)
• Clone this repo.
• cd into the repo directory.
• Run ./build.sh.
• The resulting executable will be found in bin. If you like, you can put bin on your executable search path.

Discussion

This is a proof-of-concept implementation of the Machine State Combinators idea, so it is not a full-fledged tool. Only a tiny subset of the 6502 instruction set has been implemented. But the goal was to prove out the idea, and that has been done. In the process of proving it out, some things have become clearer.

At the outset, I thought there would be some difficulties if one were to take the approach (as I initially considered) of simply defining 6502 machine code with a deep embedding in a theorem prover such as Rocq. I don't think there are, now. Fragments of 6502 code in UampirNexol simply have types. Sometimes those types prevent those fragments from being combined with other fragments, or from being valid sources from which to extract actual 6502 code. But other times they don't. This should not present any real obstacle to casting the idea in something like Rocq.

Another thing that became clearer was that the idea involves, to some extent, dependent types: a State type tracks the locations used, and in any but the simplest usage, a location is a value (much like the index of an array). The current implementation takes an ad hoc approach to typing the one instruction where this matters (STA); a proper implementation would need to implement more general (but perhaps still simplified) dependent typing.

Future directions of UampirNexol?

Now that the idea has been proved out, I don't have a definite idea where this should go next, though I have some pretty strong intuitions. Basically the language should be made more orthogonal. So along with implementing dependent typing as above, the evaluator should be regularized so that it does not assume the result of evaluation will always be a program.

The implementation could deduplicate routines and use UWord8 for bytes internally, but these are minor things.

It would be instructive to try to expand the implementation to handle a second ISA, for example the Zilog Z80, or perhaps something simpler like CHIP-8 bytecode. A certain amount of regularization of the language (as described above) would likely need to be done before that could happen.

Further Reading

• Machine State Combinators
• Function-level programming
• SixtyPical, in particular the Future directions for SixtyPical document
• COMFY-6502