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.
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).
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.
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~
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.
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.
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.
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.
The syntax in the article is not scheme, you can clearly see it in my comment you're responding to.
As for your 'light introduction' comment: even ignoring the code, these are not pedantic complaints but basic mathematical and factual errors.
For example, the statement of Birkhoff’s Representation Theorem is wrong. The article says:
> Each distributive lattice is isomorphic to an inclusion order of its join-irreducible elements.
That is simply not the theorem. The theorem says "Theorem. Any finite distributive lattice L is isomorphic to the lattice of lower sets of the partial order of the join-irreducible elements of L.". You can read the definition on Wikipedia [0]
The article is plain wrong. The join-irreducibles themselves form a poset. The theorem is about the lattice of down-sets of that poset, ordered by inclusion. So the article is NOT simplifying, but misstating one of the central results it tries to explain. Call it a 'light introduction' as long as you want. This does not excuse the article from reversing the meaning of the theorem.
It's basically like saying 'E=m*c' is a simplification of 'E=m*c^2'.
> This does not excuse the article from reversing the meaning of the theorem.
What's with this hyperbole? Even the best math books have loads of errors (typographical, factual, missing conditions, insufficient reasoning, incorrect reasoning, ...). Just look at any errata list published by any university for their set books! Nobody does this kind of hyperbole for errors in math books. Only on HN do you see this kind of takedown, which is frankly very annoying. In universities, professors and students just publish errata and focus on understanding the material, not tearing it down with such dismissive tone. It's totally unnecessary.
I don't know if you've got an axe to grind here or if you're generally this dismissive but calling it "simply not the theorem" or "plain wrong" is a very annoying kind of exaggeration that misses all nuance and human fallibility.
Yes, the precise statement of Birkhoff's representation theorem involves down-sets of the poset of join-irreducibles. Yes, the article omits that. I agree that it is imprecise.
But it's not "reversing the meaning". It still correctly points to reconstructing the lattice via an inclusion order built from join-irreducibles. What's missing is a condition. It is sloppy wording but not a fundamental error like you so want us to believe.
Feels like the productive move here is just to suggest the missing wording to the author. I'm sure they'll appreciate it. I don't really get the impulse to frame it as a takedown and be so dismissive when it's a small fix.
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.
LLMs utilize categorical distributions defined by the logits computed by the matrix multiplies, and there are many sampling strategies which are employed. This is one of the core mechanisms for token generation.
There's no peculiarity to discuss, that's how they work. That's how they are trained (the loss is defined by probabilistic density computations), that's how inference works, etc.
> 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.
I'm really surprised to hear this given the content of the post. The claims in the post are quite strong, yet here I need to give a counterargument to why the claim about consensus applying to pseudorandom processes is relevant?
I don't think it's necessary to furnish a counterexample when pointing out when a formal claim is overreaching. It's not clear what the results are in this case! So it feels premature to claim that results cover a wider array of things than shown?
For instance, this is a strong claim:
> it means that in any multi-agentic system, irrespective of how smart the agents are, they will never be able to guarantee that they are able to do both at the same time:
>
> Be Safe - i.e produce well formed software satisfying the user's specification.
> Be Live - i.e always reach consensus on the final software module.
I'm confused as to the stance, we're either hand-waving, or we're not -- so which is it?
I just came away from the read thinking that this post was pointing to something very strong and was a bit irked to find that the state of results was more subtle than the post conveys it.
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.
You’re right, there is that one example. Feels like we’re in exception that proves the rule territory. But I’d be very interested in being proven wrong! This isn’t a desire of mine, just what I’ve seen. Do you have other examples?
Also, part of my confidence comes from both having been a professional programmer for decades, across many languages, and also having programmed in Lean. It’s a great language for math, perhaps the best choice right now. But as a general purpose language it’s incredibly quirky.
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.
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.
> finite programs that run on an infinite stream of events
This requires coinduction, right? (That's my understanding of the formal representation of infinite streams.) If so, that does limit your options, since most of the proof assistants don't handle coinductive data, as I understand it.
