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.
HN generally forbids asking whether a commenter has read the article, so it's useful that you straight up admit it. you probably should read it before you ask a comment though, because as it stands, your question is not even wrong.
the blog describes a methodology for building trust in LLM-authored semantics by also proving that the semantics abstract the behaviours of a concrete binary interpreter. This pitches a way to turn compute into building useful semantics. I have no idea what or why you believed there was a relation to rust.
> HN generally forbids asking whether a commenter has read the article, so it's useful that you straight up admit it.
Nitpick, he claims he started reading it but could not finish. I also started reading it but did not finish (due to time, not the academic nature of the prose).
I'm not sure it was completely LLM-written, but it certainly wasn't as grating on the nerves like most LLM prose.
> I have no idea what or why you believed there was a relation to rust.
"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.
Yes, exactly! The point of ship your interpreter is we can take the compiled binary for a language as its ground truth. Ship in this context refers exactly to "deploying" the binary itself as opposed to building one by hand.
It's a shame that metaphor didn't make sense to you, but alas, you can't win them all.
We can argue the semantics of these words all day, but, I'm more curious, how did you find the technical content of the post?
Oh I'm sorry that it was confusing! Shipping in that sense is a common tech colloquialism. I probably should have vetted it by some ESL speakers to check accessibility for those unfamiliar with the language. That's my bad. Will take into account for the next post~
oh sorry! I didn't mean to confuse you. Ship as in shipping a piece of software. It's a colloquialism common in tech circles. In this case it refers to the fact that the git repo and proofs contain the binary artefact itself.
Instead of shipping a specification (for your language), you just ship your interpreter.
> "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.
No wonder I had trouble understanding where they were going with this!
> 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.
I was targeting the blog to a mix of both experts and non-experts. If you look at our site, Basis works on problems from a variety of domains, so the excerpt (shown on the blog listing), had to be something even non-experts could hopefully glean something out of.
i think that is a bad tradeoff. interested non-experts can use their research tool of choice. but more likely they are not going to get past the first few paragrahs. is there some reason that all posts on a blog must be understood by all readers of said blog? perhaps a tag could identify technical posts.
also, i'd expect the LLMness of that intro to bounce at least as many people as the additional context you've included retains (~0).
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
that's a shame! there's a lot of english authors, even before LLMs, who made generous use of em-dashes. You're really locking yourself out of a lot of nice literature! This blog post too~
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.
Oh, I really enjoyed that article when it came out too! I would recommend you read it before you share it next time, you might find some insights~
In this case, the GP didn't actually finish reading my article (and thus really has no standing to make any comment on its content); I assume they got filtered by the formalism, which is a shame, but I didn't want to discourage their attempts! Formal verification sometimes just isn't for everyone.
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.
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?
HN generally forbids asking whether a commenter has read the article, so it's useful that you straight up admit it. you probably should read it before you ask a comment though, because as it stands, your question is not even wrong.
the blog describes a methodology for building trust in LLM-authored semantics by also proving that the semantics abstract the behaviours of a concrete binary interpreter. This pitches a way to turn compute into building useful semantics. I have no idea what or why you believed there was a relation to rust.
> HN generally forbids asking whether a commenter has read the article, so it's useful that you straight up admit it.
Nitpick, he claims he started reading it but could not finish. I also started reading it but did not finish (due to time, not the academic nature of the prose).
I'm not sure it was completely LLM-written, but it certainly wasn't as grating on the nerves like most LLM prose.
> I have no idea what or why you believed there was a relation to rust.
TBH, I had the same question myself :-/
This is the same idea as the fixed point of the meta-circular evaluator - the abstract ideal language that lisp models almost exactly.
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.
Yes, exactly! The point of ship your interpreter is we can take the compiled binary for a language as its ground truth. Ship in this context refers exactly to "deploying" the binary itself as opposed to building one by hand.
It's a shame that metaphor didn't make sense to you, but alas, you can't win them all.
We can argue the semantics of these words all day, but, I'm more curious, how did you find the technical content of the post?
That's a really contorted argument. It's not how we use "ship" at all, and it's making your idea much harder to pick out, not easier.
Oh I'm sorry that it was confusing! Shipping in that sense is a common tech colloquialism. I probably should have vetted it by some ESL speakers to check accessibility for those unfamiliar with the language. That's my bad. Will take into account for the next post~
None of this response is making any sense to me.
Can you define what the word "ship" means in "ship your interpreter"?
oh sorry! I didn't mean to confuse you. Ship as in shipping a piece of software. It's a colloquialism common in tech circles. In this case it refers to the fact that the git repo and proofs contain the binary artefact itself.
Instead of shipping a specification (for your language), you just ship your interpreter.
I think you're using the word wrong.
> "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.
No wonder I had trouble understanding where they were going with this!
> 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.
I was targeting the blog to a mix of both experts and non-experts. If you look at our site, Basis works on problems from a variety of domains, so the excerpt (shown on the blog listing), had to be something even non-experts could hopefully glean something out of.
i think that is a bad tradeoff. interested non-experts can use their research tool of choice. but more likely they are not going to get past the first few paragrahs. is there some reason that all posts on a blog must be understood by all readers of said blog? perhaps a tag could identify technical posts.
also, i'd expect the LLMness of that intro to bounce at least as many people as the additional context you've included retains (~0).
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
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
that's a shame! there's a lot of english authors, even before LLMs, who made generous use of em-dashes. You're really locking yourself out of a lot of nice literature! This blog post too~
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.
that's a shame~ there's a really fun idea buried in there! sometimes some people just aren't cut out to handle formal reasoning and that's okay!
a lot of human effort clearly went into this work. so the term "slop" is harsh. but its also a bad look to lash out at that label and claim that people Just Don't Get It. check out https://bcantrill.dtrace.org/2025/12/05/your-intellectual-fl...
Oh, I really enjoyed that article when it came out too! I would recommend you read it before you share it next time, you might find some insights~
In this case, the GP didn't actually finish reading my article (and thus really has no standing to make any comment on its content); I assume they got filtered by the formalism, which is a shame, but I didn't want to discourage their attempts! Formal verification sometimes just isn't for everyone.
would you be willing to be more specific on what insights i've missed?
regarding the GP's comments on article content, i suppose maybe one critique could have been sharpened by a closer reading?
> There could be some value buried in there
i'd imagine you agree.
> could have been 10% of its size
likely false, but i interpreted this as an intentional exaggeration
> could have been human written
likely true