This is great. Many people online who "verify their software" seem to just tell an LLM "verify dis" and have no idea what comes out. The model could be proving 1+1=2 for all they know.<p>These guys actually show some Lean theorems they proved. Also interesting approach to compile the existing interpreter into the de-facto spec.
I am not sure what I have read here, I couldn't finish it, due to the AI writing. But you do have to wonder - Isn't this (just) a subset of Rust?
This is AI slop.<p>"Ship" in software means placing the interpreter into the release bundle, but here it is meant to refer to taking the interpreter as ground truth for formal verification (as opposed to a pristine spec), which sounds like incoherent AI writing.<p>Usually metaphors are meant to make things easier to understand not harder.
> We had LLMs write precise mathematical rules, or a formal semantics, for how a small programming language should behave. We then used Lean, a tool for checking mathematical proofs, to prove that the interpreter—the program that runs code written in that language—follows those rules even after being compiled into low-level instructions understood by a RISC-V computer chip.<p>who is your audience? why are you defining every single term here? perhaps i am less tenacious than most, but i wouldn't expect many who are unfamiliar with interpreters, formal proofs, or assembly language to be willing to charge on ahead—even when armed with that additional context.<p>also, writing your very first paragraph via LLM is certainly a choice.