gopiandcode

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

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.

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

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!

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?

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.