Ship Your Interpreter
Summary
Basis explores the use of large language models to develop formal semantics for a small programming language and then verifies the interpreter against a RISC-V binary using Lean. It discusses memory reasoning with separation logic, four on-top tools (type checker, program logic, abstract interpreter, verified compiler), and plans to scale the approach to Lua, OCaml, and CPython.