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.

> an untyped closure-based programming language with a similar array and sort api to JS

Ah! You're talking about Racket or Scheme!

```

> (sort '(3 1 2) (lambda (a b) (< a b)))

'(1,2,3)

```

I suppose you ought to go and tell the r6rs standardisation team that a HN user vehemently disagrees with their api: https://www.r6rs.org/document/lib-html-5.96/r6rs-lib-Z-H-5.h...

To address your actual pedantry, clearly you have some implicit normative belief about how a book about category theory should be written. That's cool, but this book has clearly chosen another approach, and appears to be clear and well explained enough to give a light introduction to category theory.

If you're pushing me, let's say we're not hand waving then. LLMs, abstraction removed, are deterministic computations of matrix-multiplication, f(x) -> y. If you want, we can make them pseudo-random, but thus still a deterministic process. FLP then holds. I'm not sure what your confusion is.

It really depends on your model in my opinion.

At the lowest level of abstraction, LLMs are just matrix multiplication. Deterministic functions of their inputs. Of course, we can argue on the details and specifics of how the peculiarities of inference in practice lead to non-deterministic behaviours but now our model is being complicated by vague aspects of reality.

One convenient way of sidestepping these is to model them as random functions, sure. I wouldn't go as far to say they are "inherently stochastic creatures". Maybe that's the case, but you haven't really given substantial evidence to justify that claim.

At a higher level of abstraction, one possible model of llms is as deterministic functions of their inputs again, but now as functions of token streams or higher abstractions like sentences rather than the underlying matrix multiplication. In this case again we expect llms to produce roughly consistent outputs given the same prompt. In this case, again, we can apply deterministic theorems.

I guess my central claim is that there hasn't been a salient argument made as to why the randomness here is relevant for consensus. Maybe the models exhibit some variability in their output, but in practice does this substantially change how they approach consensus? Can we model this as artefacts of how they are initialised rather than some inherent stochasticity? Why not? It feels like randomness is being introduced here as a sort of magic "get out of jail" free card here.

Just my two cents I suppose.

As quoted in the article itself, please take it up with the chief architect of the Lean FRO:

> ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct.

> Not tested. Proved. For every possible input. lean-zip

Where are you coming up with this from? This is awfully confident for a fact you seem to have conjured up without evidence. As far as I am aware, Lean is interested in being used as a programming language (see: https://lean-lang.org/functional_programming_in_lean/) and people are deploying Lean in production: https://docs.aws.amazon.com/clean-rooms/latest/userguide/dif...

Yes, here's a concrete example: https://github.com/leanprover/SampCert This is an implementation of a verified sampler, in lean. Not an embedding in some other language. The implementation itself is in lean, and a python ffi is used to call into the verified implementation. I don't know if AWS is big enough for your standards, but here is at least one example. Besides that, I'm more reporting on the general vibe I have observed from numerous talks at AI4maths workshops at Neurips, at the DARPA AI4Math ExpMath kickoff, etc. People are considering Lean as a serious programming language. Maybe that's surprising to the mathematicians, but as a PL person, I find the language really nicely designed and I can understand why people want to write in it.

Right, but what you're describing is a consensus protocol. It's called 2 phase commit. The point of the article is just that we should really be analysing these high level plans in terms of distributed algorithms terms, because there are fundamental limitations that you can't overcome.

Lean-zip was not my project but one by others in the lean community. I'm not sure about the methodological details of their process - you might want to check with the original lean-zip authors (https://github.com/kim-em/lean-zip)

It does seem that way doesn't it? But as software bugs are becoming easier to find and exploit, I'm expecting more and more people, including those not "sophisticated enough" to understand and employ formal verification to start using it

Sorry, I'm not sure I follow. We are talking about bugs in a verified system, that is, in this case, a verified implementation of a zlib-based compression tool. Did it have bugs? yes. Several in fact. I'd recommend reading the article for a detailed listing of the bugs in the tool.

you can still verify arbitrarily long running programs - there are instances of such software, such as sel4 (https://sel4.systems/) and certikos (https://flint.cs.yale.edu/certikos/), you simply model them as finite programs that run on an infinite stream of events.

Repeating myself, when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target.

If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs.

Second, there was a bug in the code. Maybe not a functional correctness bug, but I, along with many and most end users, would consider a crashing program buggy. Maybe we just have different tastes or different standards on what we consider an acceptable level of software quality.

W.r.t people running Lean in production, you'd be surprised...

Hi! Author here. When we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target.

If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs.

Secondly, I did find a bug in the algorithm. in Archive.lean, in the parsing of the compressed archive headers. That was the crashing input.