Scalable formal machine models

In the past few years, we have seen machine-checked proofs of relatively large software systems, including compilers and micro-kernels. But like all formal arguments, the assurance gained by these mechanical proofs is only as good as the models we construct of the underlying machine. I will argue that how we construct and validate these models is of vital importance for the research community. In particular, I propose that we develop domain-specific languages (DSLs) for describing the semantics of machines, and build interpretations of these DSLs in our respective proof-development systems. This will allow us to factor out and re-use machine semantics for everything from software to hardware.