gopiandcode

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.

If it has become a cult, it's become a cult that has infiltrated so far as DARPA - see their TRACTOR program (https://www.darpa.mil/research/programs/translating-all-c-to...)

I think couching the success and excitement around rust to ideology or a "cult" as you say is somewhat digging your head into the sand. There are concrete facts and results. Rust is empirically producing levels of memory safety that humanity did not think was possible with software at scale. This is truly groundbreaking.

So to clarify, the crusade to rewrite things in Rust is not my fight. To be honest, I'm more a third party watching from the sidelines. There seems to be big institutional interest in replacing C with Rust. Not for ideological reasons. Just for plain economic ones. Rust code is breaking industry standards of memory safety/bug density/review time. I link it in the article, but for example, darpa has a recent big grant program, TRACTOR: Translating All C to Rust (https://www.darpa.mil/research/programs/translating-all-c-to...).

My article was more a commentary aimed at the efforts towards doing that. In some sense arguing that there are some foundational formal deficiencies currently that mean that it's not even clear what success would be. I guess I don't really take a position on the value of rewriting things into Rust, aside from adopting the views of these existing programs as some prelude.

w.r.t the first point, so ideally you wouldn't want to do that because it'd incur a heavy runtime performance. Rust's memory analysis allows eliminating those kinds of memory bugs without having to check writes at runtime.

w.r.t the second point, I talk a bit about that in the article itself -- the fundamental problem right now is that there's no real formal way of even stating what it means to correctly translate a program from C to Rust. We could maybe have a smart LLM that translates things to Rust, but would you trust it without tests? or ideally a proof of correctness? what properties should we test? etc.

oh yep, it's definitely more than usable for 'actual programming' beyond just maths proofs.

Things like:

- bindings to godot (https://github.com/kiranandcode/lean4-godot)

- advent of code (https://github.com/kiranandcode/lean-aoc)

- ffi bindings to constraint solvers (https://github.com/kiranandcode/cleango/)

Obviously a slightly biased selection here, but the key point is to clarify that it's more than feasible to use it for real programs that do all sorts of non-mathy stuff.

Arguably it really depends on your DSL right? If it has a semantics that already lies close to existing programming languages, then I'd agree that a few examples might be sufficient, but what if your particular domain doesn't match as closely?

Examples of domains that might be more challenging to design DSLs for: languages for knitting, non-deterministic languages to represent streaming etc. (i.e https://pldi25.sigplan.org/details/pldi-2025-papers/50/Funct... )

My main concern is that LLMs might excel at the mundane tasks, but struggle at the more exciting advances, and so now the activation energy for coming up with advances DSLs is going to increase and as a result, the field might stagnate.

Oh that's a great blog post and a very interesting point. Yep, I hadn't considered how LLMs would affect frameworks in existing languages, but it makes sense that there's a very similar effect of reinforcing the incumbents and stifling innovation.

I'd argue that the problem of solving this effect in DSLs might be a bit harder than for frameworks, because DSLs can have wildly different semantics (imagine for example a logic programming DSL a la prolog, vs a functional DSL a la haskell), so these don't fit as nicely into the framework of MCPs maybe. I agree that it's not unsolvable though, but it definitely needs more research into.

mhhm yes yes. There's a thread of discussion that I didn't quite chose to delve into in the post, but there is something interesting to be found in the observation that languages that are close to natural language (Python being famous for being almost executable pseudo-code for a while) being easier for LLMs to generate.

Maybe designing new languages to be close to pseudo-code might lead to better results in terms of asking LLMs to generate them? but there's also a fear that maybe prose-like syntax might not be the most appropriate for some problem domains.

Ahh, that is a valid point; so it's not quite as clear as using something like quick check, but it does feel like there is increasing interest and activity in people trying out doing exploratory maths in Lean itself.

I mention it in the blog post, but one project in that direction is Terence Tao's equational_theories project (https://teorth.github.io/equational_theories/), where it seems like a bunch of hobbyists and mathematicians are working together using Lean to prove new mathematics enabled by Lean.

Fwiw there's also an Emacs plugin which is what I use and it works really well.

For using Lean as a theorem prover, this book is pretty good: https://github.com/lean-forward/logical_verification_2024

Also, Lean is also remarkably usable as a programming language itself, which might give an easier onboarding ramp: https://lean-lang.org/functional_programming_in_lean/

Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd be really eager to try that out.

e.g.:

- embedding a prolog/asp DSL: https://github.com/kiranandcode/cleango

- embedding a tex/latex DSL: https://github.com/kiranandcode/LeanTeX

I am more than aware of Typescript, you seem to have misunderstood my point: I was not describing a particular type system (of which there have been many of this ilk) but rather conjecturing that targeting interfaces specifically might make LLM-based code generation/type inference more effective.

The visualisation of how the model sees nullability was fascinating.

I'm curious if this probing of nullability could be composed with other LLM/ML-based python-typing tools to improve their accuracy.

Maybe even focusing on interfaces such as nullability rather than precise types would work better with a duck-typed language like python than inferring types directly (i.e we don't really care if a variable is an int specifically, but rather that it supports _add or _sub etc. that it is numeric).

I find this particular choice of syntax somewhat amusing because the pipe notation based query construction was something I ended up using a year ago when making an SQL library in OCaml:

https://github.com/kiranandcode/petrol

An example query being:

```

let insert_person ~name:n ~age:a db = Query.insert ~table:example_table ~values:Expr.[ name := s n; age := i a ] |> Request.make_zero |> Petrol.exec db

```

Please also consider how much less inclusive and accessible computing would be if access to development tooling was placed behind such exorbitantly priced paywalls... The things we have at the moment aren't perfect, but I feel like the fact that the barrier of entry to programming is so low is an overwhelming positive that I couldn't see any level of bells and whistles justifying taking it away.

To be fair, the distinction here is about actions by a government, versus actions by private entities. Opposition to the government banning a website does not necessarily mean that you would oppose private companies refusing to provide service to a bad actor.

If not, how do you reconcile this belief with the right of scientists and publishers to sell their productive labor?

As many others in the thread have said - the profits from the paper paywalls go to the publishers, reviewing is done by volunteers.

As an aside, it's funny how often defenders of intellectual slavery are so dug in to their beliefs while being completely unaware of the mechanisms of what they're defending. I suppose such ignorance is a necessary precondition to support such injustice.

Funny you should mention that - I actually ran into another in-proportion solar system park model in Eugene, Oregon, USA: https://eugenesciencecenter.org/exhibits/eugene-solar-system...