> 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.
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.
also, writing your very first paragraph via LLM is certainly a choice.
my brain ejects out of my skull when i see the EM dash. it's sort of insane to me people are willing to use LLM's to make stuff, but they can't even take the time to write why they think it's a valuable contribution. the shortcutting is off the charts, and this and a sea of other things shall go into the no thanks bin
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.
also, writing your very first paragraph via LLM is certainly a choice.