Assembly for virtual computer running on Lean

Stream: general

[Jihoon Hyun]

I kept thinking of a virtual computer based on a basic von Neumann model (maybe turing machine suffices?) implemented on Lean, and an assembly running on the computer. It's just an idea, so I ask if there is a project like this, and if this project looks feasible. It should be highly related to computability and complexity theory, as we can count the number of assembly instructions to measure complexity.

[Shreyas Srinivas]

Read the mehlhorn and sanders book. They have a very precise model in the first chapter: https://people.mpi-inf.mpg.de/~mehlhorn/Toolbox.html

[Shreyas Srinivas]

EDIT: Better book : vol 1 chapter 1 of this book : https://people.mpi-inf.mpg.de/~mehlhorn/DatAlgbooks.html

[Shreyas Srinivas]

They give a precise machine model

[Jihoon Hyun]

Thank you for the resource! I'll take a look at it.