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~

No, it very much is not unless your descriptions are entirely unrepresentative of what you actually mean to say.

I'm well aware of how it is used in tech - I've worked in tech for 30+ years.

And frankly, your insulting comments here undermine you further. My English comprehension is well above the average native English speaker, and judging by your comments here I'm not confident I can say the same about yours.

Consider that when multiple people here have issues with understanding you, it says something about your language use, not theirs.

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!