YHK - yet another hacker news clone

Ship Your Interpreter

18 points gopiandcode 1 day ago 7 comments

skavi 1 hour ago | parent

> 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.

artemonster 1 hour ago | parent

I couldnt finish this slop. There is could be some value buried in there, but it could have been 10% of its size and human written

trueno 1 hour ago | parent

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

hnlmorg 30 minutes ago | parent

I agree with your general point but I really hate that the em dash has become so hated because it’s something I use commonly and have done before GPTs.

Same goes for the Oxford comma too.

ngruhn 1 hour ago | parent

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.

These guys actually show some Lean theorems they proved. Also interesting approach to compile the existing interpreter into the de-facto spec.

ISackKnights 35 minutes ago | parent

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?

imtringued 22 minutes ago | parent

This is AI slop.

"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.

Usually metaphors are meant to make things easier to understand not harder.