pron

I was implying nothing of the sort. It is an important and serious kernel, but a very small one and a very simple one, which it had to be so it could be verified, like the har-realtime safety critical software I worked on and formally verified. We don't yet know how to verify non-small or non-simple software with formal proofs, and unfortunately, the gap in size between the software we can prove and the average software we write has only grown significantly over the past 40 years. If AI knows how to verify "average software", then it certainly doesn't need our help with software tasks that are far simpler. My point was that some companies are imagining an AI that can write software like humans never could and then suggesting they can help it by writing simple software tools.

Many languages can do that (Ada SPARK, Dafny, even Java with JML, and quite a few more), but there are really two languages here, the spec language and the program language. The spec language isn't executable, and the program language doesn't spec. What TLA+ does is offer a a single continuum, with a language that's much simpler than both Eiffel's spec language and its program language, and can describe anything at arbitrary precision. It can describe the QS algorithm in general, and it can describe the activations of the logic gates in the CPU as a specific QS runs on a specific machine, and it can take any description of QS, at any level, and show the abstraction/implementation between them. Again, this is all in a language that's much simpler than Python, and that allows reasoning directly in the language because it supports substitution and all the normal manipulation capabilities we expect from mathematical formulas.

In general, problems whose solutions are easily checkable are not necessarily easily solvable, and the difficulty of finding the proof also depends on how the software is written, which is why humans, at least, don't try to prove arbitrary programs correct, but write the program and the proof together. But regardless, the tools involved are really not very complicated. While it's possible, I find it hard to justify betting on AI being able to prove a 100KLOC-10MLOC program correct while not being able to write a 10KLOC tool well enough.

Maybe (for humans the two often go together), but what's the hypothesis behind assuming it will do the one and not the other? It seems like a very specific and arbitrary bet, not much unlike betting that AI will be able to learn English but not French.

I'm totally with you, but that's not quite what this company and others are trying to do based on their marketing material.

If you're talking about seL4, it is tiny and intentionally simplified. I'm not aware of programs larger than ~10KLOC that have ever been verified end-to-end.

TLA+ is not a model checker. It's a general language for writing mathematics, akin to Lean, only Lean focuses on high mathematics while TLA+ focuses on dynamic systems. There are a proof checker and at least one model checker that work on subsets of TLA+.

As to why TLA+ is better at describing systems than programming languages, the reason is that it's much more general. It can say things like "a routine that sorts in a quadratic number of steps or less" rather than a specific sorting algorithm, and it allows stating (and proving) that a specific sorting algorithm matches that description or not. Most TLA+ formulas are too abstract to be run by a computer (i.e. they describe too many potential algorithms), but that's exactly what makes them useful to describe things when either you don't care about the details or you want to show that a particular algorithm implements a general property.

BTW, even algorithms like Quicksort are, themselves, too general to be accurately described by a programming language (i.e. a language that can be executed). Quicksort doesn't specify how a pivot is chosen (it doesn't matter for the correctness), it doesn't specify how that partitioning is done (ditto), and it doesn't specify in what order the recursion is done or perhaps even in parallel (ditto). Yet a computer needs to be told all these details to run an implementation of Quicksort, even though the algorithm works, and can be proven to work, no matter what these details are. In a language like TLA+ you can say how to choose a pivot or you can say "a pivot is somehow chosen" (which covers all possible mechanisms for choosing one).

Also, TLA+ is much simpler than a programming language and obeys simple and intuitive substitution rules - e.g. `x = 3` is equivalent to `3 = x` and `x = y + 1` is (almost) equivalent to `x - y = 1`, which is what you want when you're after clarity. It's just different from programming languages (because it's maths), so it's a different, though simpler, kind of language to learn.

I love TLA+ to describe systems precisely yet succinctly and reason about them. But as someone who's been using formal methods to help software development for many years, this whole industry around tools to connect such a wonderful mathematical language and others like it, like Lean, with AI, to the point of hiding the reasoning from people, confuses me.

Proving programs correct end-to-end (i.e. code to high-level properties) - as this company and others purport to do - is so difficult that humans have only been able to do it for very small programs (~10KLOC) and even then, in very specialised cases, where the programs have been written in an extra-simple way (often at the cost of performance, because performance often requires more complicated algorithms). If AI becomes at least an order of magnitude more capable than humans at software development, which is what will be required for this task, would it need our help to write various tools and harnesses that help with the task? After all, writing these tools is so much easier than using them for that goal that I don't understand the hypothesis behind AI capability here.

This company says: they're "developing the agentic frameworks to make these correctness guarantees accessible to all software engineers". But developing all that is the easy part! If AI can do the hard part, why does it need our help to make this accessible, it can surely find a way to do that easy part itself! It's like saying, "Soon we'll have a machine that can harness so much energy to boil an ocean; we've built a service that lets you order a taxi to take the machine to the beach!" Why would an AI that is so much better than us at writing software need our help writing any kind of software for it?

It seems more Oracle than Gluon: https://github.com/openjdk/jfx/graphs/contributors

> As far as I understand it comptime is basically runtime compilation and integration into the running program (just-in-time compilation). That gives it great flexibility of course but it also requires each Zig application to carry a full compiler inside of it.

Well, it isn't that and it doesn't require that.

> I don't understand your C++ example about it getting slower and needing to "move pointers."

Because low-level languages need to use machine pointers, their dynamic heap allocations have a high CPU overhead; it's that overhead that moving GCs are designed to reduce, but because they move pointers, using them requires an FFI between these pointers and machine pointers. This is why in low level languages we try to avoid dynamic allocations when we can, but that increases long-term maintenance costs.

Well, the problems don't start after 20 years but after 5 or so (depending on the size of the codebase and the rate of the application's evolution), and the reason there aren't many large and oldish Rust codebases isn't because the language is too young for that (work on it began twenty years ago, and it's been stable for over a decade); that's middle-aged for a programming language. When C++ was of a similar age, there were thousands of >1MLOC programs written in it. One reason is obviously because when C++ was of the same age, there weren't as many suitable high-level alternatives, and people just don't pick a low-level language for most large applications anymore. But most Rust fans at least on social media, have not actually had much experience with it or with low-level programming in general; I'm guessing most haven't worked on Rust projects with more than 10 full-time people on them (this isn't normal in the industry, BTW, as a lot of software lives in large programs). And again, there are people who can certainly live with these issues, but they are real, and many certainly find them troubling.

It's not theoretical, it's one of the main reasons many large applications abandoned C++, and there's absolutely no reason for it to not exist in Rust. All low-level languages suffer from expensive evolution for fundamental reasons - the reliance on an AOT compiler and the lack of movable pointers impose serious performance tradeoffs in large programs. Optimising JITs and moving GCs were invented, in large part, to address this very real problem, familiar to many low-level programmers who have maintained large codebases for a long time. It's also why large runtimes like TCMalloc were invented to assist as much as they can.

Most actual Rust programmers haven't maintained a large Rust program for a long time. Now, don't get me wrong - there are many C++ programmers who are fine with it, but many who aren't. What I find annoying is people without much experience in Rust assuming that everyone or almost everyone should like it, even though that's never been true for any language. I'm not saying Rust is bad by any means; in fact, I think it's better than C++ in a few ways. I'm explaining why I don't like it.

sorry, the "and" was a typo

> But this should be up and front in their self-promotion!

It is! "A fresh approach to metaprogramming based on compile-time code execution and lazy evaluation" is the second selling point after simplicity: https://ziglang.org

Obviously, they can't call it partial evaluation because not many people know what that is. Zig's approach was eye opening to me. I'm very familiar with how macros are used in Scheme, but comptime is intentionally weaker (unlike macros, it's referentially transparent, so strictly weaker) and I was surprised by just how far it can go. It's not everyday that you see a new kind of a partial evaluation construct, let alone a language that's almost entirely based on it (like Lisp only for comptime).

For me it's because Zig presents a novel and even revolutionary new coherent design for low-level programming, whereas D is mostly a collection of many ideas, many of them are good, but they don't coalesce into a simple design philosophy. I think somebody once said that good (or coherent) design is what happens not when there's nothing left to add but when there's nothing left to remove. That product X has all the components of product Y and possibly more doesn't mean that it contains within it Y's design. The novelty of the iPhone wasn't that it had a touchscreen, but that it had little else. Such a coherent design grabs, and deserves, attention.

For example, another language that immediately grabbed my attention (aspirationally; I haven't looked at it closely yet) is https://github.com/aardappel/goose/. That's not because it has arenas, but because it doesn't have anything else.

Benign write/write races (when multiple threads do unordered writes of the same value to the same address) are quite common and useful, both in parallel algorithms and in lazy initialisation. Useful benign read/write races are far more rare to the point I'd say it's ok to assume they don't (or shouldn't) exist.

However, in C and C++ (and Rust) benign non-atomic write/write races are UB (indeed, LLVM also treats them as potential causes of UB). In C# and in Java they are safe (although Java currently only has non-atomic writes on 32-bit machines, but soon they'll be more common when value types are enhanced). LLVM even has a specific construct to support the Java-style memory model (https://llvm.org/docs/Atomics.html#unordered), and Zig lets you use it (https://ziglang.org/documentation/master/#atomicStore).

> i find it fascinating how big of a rust hater you are. willing to outright lie to make your point.. because you can do this with_allocator

You say I outright lie for not mentioning the existence of something that doesn't exist??? I guess you're saying it's possible to create such a mechanism (or that some libraries do create ad-hoc ones), but that's not the point.

> there is nothing stopping you from using custom allocators with your own code or with calls to thirdparty dependencies

I didn't say there's anything in the language stopping C++ and Rust from having such a standard library and ecosystem of libraries. They just don't have that yet.

> if your language is not memory safe and you need to manage memory yourself, they're more important. but this isn't the case with rust. c and zig folks are obsessed with arena allocators particularly because they can group lifetimes of individual objects, reducing the amount of malloc/free calls and thus the amount of use after free, double free, nullptr derefs, or leaks that can occur. n rust this isn't a concern so custom allocators are only used for performance reasons.

This is simply untrue. I won't call it an outright lie, as it's probably just a lack of experience with low-level programming.

First, I'm trying to point out the problems we've had in C++, most of which only became apparent when evolving large codebases over time. People who have not had experience evolving large C++ or Rust codebases over years simply don't know about these problems and certainly can't claim they don't exist. Writing smaller programs in C++ or even large but young programs has always been a pleasure. The language is expressive and productive. Some of the biggest issues only arise years later, when the program gets either expensive to maintain or slow.

Second, experienced C and C++ folks cannot be "obsessed" with arenas for the reasons you mentioned because until maybe 20 or even 15 years ago memory safety wasn't a widespread obsession. It was a correctness issue like all others, and its outsized role as the cause of security vulnerabilities wasn't widely known until more recently.

Lastly, you don't pick Rust for safety. Most software in the world today is already written in languages that are at least as memory-safe safe as Rust, sometimes more so. These days, you pick C, or C++, or Rust, or Zig when you want to do something that's largely low-level. Things that are low-level often also need to be reasonably fast, and large low-level codebases that evolve over years tend to suffer serious performance issues because of memory management (because, being low-level, they can't move pointers and so can't use things like a moving GC to reduce the overheads of their malloc/free runtimes; this is why companies with actual experience with long-maintained large low-level codebases make huge runtimes like TCMalloc to help them to a degree, which you also may not have needed yet), and arenas are the primary way to get memory performance similar to what you see with modern moving GCs (and even somewhat better).

Now, you could say that C++ only started moving in that direction with pmr in C++ 17, and that's true. But the need was recognised as early as 2005, traditionally C++ codebases didn't rely on many libraries so interoperability has typically not been a large concern, and the number of large C++ programs that would benefit from such a thing declined over the years because of the low-level maintenance issues I mentioned and the growing availability of fast high-level languages.

My distaste for Rust isn't because I like C++ so much. Even though it's been one of my primary programming languages for the past 25 years, I "hate" it for the very same reasons. Most Rust superfans are people who have not had enough experience with it and they don't know about the problems. Not all, of course, and even C++ has superfans, which is why I said that among the people who are experienced in low-level programming, there are people who like the C++/Rust approach (of trying to make low-level code appear high-level) and people who don't.

It is entirely novel. As I wrote, what makes the design revolutionary isn't the partial evaluation mechanism itself, but how the language is organised around it. It's like what made the iPhone's design revolutionary wasn't that it had a touchscreen, but that it didn't have a keypad. Partial evaluation mechanisms aren't very interesting in themselves; what's interesting is building a language around a unified partial evaluation mechanism and little else. But yes, D gets credit for adding more partial evaluation features.

This is true. In Java, we have a notion we call "integrity", which is a generalisation of memory safety and includes a host of properties guaranteed by the platform. It includes memory safety, but also things like "a non-public method cannot be called or a non-public field cannot be accessed (even reflectively) by code in another module".

To address the problem that once integrity can be violated anywhere, only global analysis can prove that nothing bad happens, we've done two things:

1. We require the application to explicitly permit any integrity violation by a module; i.e. a library can't allow itself to violate integrity. This is a principle we call "Integrity by Default" (https://openjdk.org/jeps/8305968).

2. We try to minimise the need for potential integrity violations (this is very different from Rust, which requires unsafe even for things like benign write/write races, which are fairly common, and various basic data structures). Over the years we've offered safe replacements for things that used to require Unsafe. In other words, clearly demarcating unsafe code isn't enough if it's needed at all in many situations.

It isn't perfect, of course, as some libraries do require unsafe operations for direct interaction with native code or with memory, but their number has been greatly reduced, and they cannot do this without the application's explicit approval. Interestingly, this has annoyed library authors who want to do unsafe things but don't want to application authors to be alarmed because "we know what we're doing," and it's also annoyed some application authors who want to use such libraries and are forced to explicitly add permissions. But I think that the community, as a whole, has eventually accepted this because the harm done to those who don't care is small (they just need to add the permissions), to those who do care it helps a lot, and because fewer and fewer libraries require "integrity-busting" permissions, many applications need to do absolutely nothing and get important guarantees for free.

Many more C programs have been verified than Rust programs. Also, Zig's spatial and memory safety is as good as Rust's, so it's not really similar to C at all.

The reason it's not "the norm" is that (especially with spatial safety taken care of), not every line is equally dangerous at all. Still, there's no doubt that more guarantees help, but that is only when all other things are equal. If you pick a low-level language for mostly low-level things, so Rust doesn't offer safety for the trickiest code, and furthermore it makes certain things harder to see because the language is more complicated, then things become much less clear. Obviously, when the vast majority of the trickiest, most important code doesn't need to be low-level, Rust would probably be safer on the whole, but in such situations I see no reason to choose either Rust or Zig. You need to choose a low-level language if the core of what you're doing needs to be low-level.

When that is the case (and it isn't yet; and remember that it's not only the containers, and strings, that need to be parameterised, but any routine that allocates them, transitively), then that's what Zig does. But the question was doesn't Rust solve memory management already, and this is an important aspect it clearly doesn't solve just yet.

I don't know exactly how specific you want to be, but sure, because we've come across this countless times in C++, which suffers from the exact same problem.

Suppose you're writing a program that's mostly high-level, say some kind of concurrent server, and it's large-ish, say around 1MLOC (most C++ programs I've worked on were significantly larger). Because the language is also a low-level language, it has low-level constraints, so:

1. It needs to use an AOT compiler, and consequently to get good performance you need to use less general mechanisms, such as direct (as opposed to dynamic) dispatch and even manual monorphisation (with generics/templates). These are viral, so they have to be carefully chosen (you can't monomorphise everything or you'll get machine code explosion). Five years later you need to make a big change that requires more generality, and then you either have to reconsider all of your manual optimisations, which is expensive, or go for more general constructs (dynamic dispatch) and the program gets slower.

2. It needs to use machine pointers (i.e. you can't enjoy a moving GC), and so you try to use the stack as much as possible (which you can't really do for anything dynamic), or suffer the high cost of malloc/free on individual objects. As the program evolves, you need to make things more general, and objects that could live on the stack now need to go on the heap, and objects that lived on the heap now may need to be shared among threads, in which case you often add the additional cost of refcounting GC. Of course, you want to use arenas in many cases, but they're very, very hard to use in C++ and Rust.

You'd be better off - performance-wise and maintenance-wise - with a good optimising JIT and a moving GC. This was exactly a problem with many C++ programs that didn't really need a lot of direct hardware interaction - everything worked great for a few years, and then the evolution and maintenance costs became really high (or the programs became slow).

Now suppose you're writing something low-level, i.e. you really need to interact with the hardware and/or OS directly a lot, and want to control everything - where everything is in memory, exactly when it's initialised, exactly when it's freed, exactly which operations are executed and when. But now you have a language that's also high-level, so it has a lot of implicitness that hides from you the things you want to see (and in Rust's case, you lose the safety). Best case scenario, you rely on disciplne and avoid implicit features, but then you also need to avoid much of the standard library.

Anyway, combining high and low level in the same language was C++'s dream: one language for everything. Of course, for a while we didn't know about the maintenance problems, as those appear only years down the line, but more importantly, there weren't really high-performance high-level languages back then. These days, with lessons learnt and with more options, I prefer a language that focuses on being high-level for high-level stuff, and a language that focuses on low-level for low-level stuff. If you really need both kinds, use two languages.

> but rust has crates like bumpalo for that purpose.

Except that's not composable - not only do you need specialised data structures, but all (transitively) allocating calls need to be specialised. That's the exact same issue we have in C++, and that's the issue Zig seeks to address. BTW, just the other day there was a post here about a language with another interesting approach, but I have yet to give it a close look: https://github.com/aardappel/goose/

> But I'm mostly working on HPC-style code where I don't have to do with wildly varying input or output sizes.

There you have it. The problems arise more quickly in concurrent rather than parallel code, and when there are lots of features added over the years that touch the hot paths.

> in-memory DB server

Actually, here there can be big problems (as it's also about concurrency rather than parallelism). Last week a colleague of mine looked at Moka and saw that it could only offer half the throughput as Java's Caffeine at the same latency and RAM footprint (almost; the Java program used 5% more RAM). When he looked into it, he saw that over 40% of the program's CPU was spent on the epoch-based reclamation.

They're not separate forms but they are separate modes, and it is precisely because the language tries to fit both these modes into the same language that both suffer. I fully understand the goal of trying to unify these modes into the same language (C++ does the same thing), but there have always been very experienced people who like this approach and those who dislike it, hence it's not "solved". Something is solved when there's a broad consensus it's solved, and there isn't one here.

I mean, someone can think it's solved for them, but if they're asking why others don't see it the same way and why many expert low-level programmers are at least intrigued by Zig, this is why. I prefer a simpler high-performance high-level language for high-level things, and a simpler low-level language for low-level things, and I dislike the C++/Rust approach of combining them into one complicated language. Some may think you get the best of both worlds; others, like me, think you get the worst of both worlds.

That's always been true in all the safe languages with unsafe escape hatches, except here these "primitives" are the main reason to reach for a low-level language in the first place - because they presumably require the control that low-level languages offer. Combining them in the same language might appeal to some and not to others who think that the high-level, safe parts are unnecessarily complicated because it needs to integrate with the low-level parts, and the low-level parts are unnecessarily complicated because they need to integrate with the safe parts. Anyway, some like this and some don't, but my point is that it's not "mostly solved".

> What are you talking about? I've never encountered this and I've been using Rust for 10 years.

Okay, but I've been doing low-level programming professionally for 25 years, and have encountered this over and over in large programs (over 500KLOC) as they evolve.

> I don't understand the hype about Zig?

As a long-time low-level programmer, and as someone working on a popular mainstream language, I find Zig fascinating, and I also think it addresses a long-standing problem in low-level programming. I'll get to the problem later, but the fascinating part is its use of partial evaluation (comptime) as a single coherent mechanism that replaces a myriad of other partial-evaluation mechanisms (macros, templates/generics, constexprs). That one mechanism is the core of the language, like macros are in lisps, and that design - whether you like it or not - is revolutionary. It's never been done before (other languages have partial evaluation mechanisms that are almost as general, but they're offered in addition to, not as a replacement of, other features).

> rust mostly-solved the memory management problem at compile time and without a GC

"Mostly" does a lot of work here because 1., if you look at the implementation of very efficient, possibly specialised data structures - the very thing you reach for a low-level language for - they typically require unsafe, and 2., it still suffers from the problem C++ has had for decades, which is that over time, as program changes and evolves over years, things tend to drift toward the more general mechanisms that rely on malloc/free on an individual objects, and the program gets slower and slower (huge runtimes like TCMalloc help, but not enough, because they can't move pointers). This problem, of programs that start out fast, but after five or ten years of evolution need to spend a lot of effort to remain fast, is one of the things moving collectors were designed to solve, but they require moving pointers, which doesn't work in low-level languages that are not meant to have an FFI layer between them and the hardware.

To compete with the performance of moving GCs, which allocate through bumping a pointer, like on the stack, and free memory in bulk, low-level languages need to rely on arenas (which work based on a similar principle), and Zig is the first language that makes arenas almost user-friendly and hopefully sufficiently composable to withstand program evolution. Of course, time will tell how well this works in practice.

> But if it needs one language for programming, machine code, why is that the optimal and only one for every application?

Why would any other specific language be? Machine code is the most general and, as I said, if the AI wants to use a compiler to, say, help generate code for other platforms, it can create one.

> Also predicate logic can be expressed using machine code

It can't. Predicate logic has certain deduction rules, and these rules are different from those of machine code (e.g. machine code doesn't have quantifiers or their introduction and elimination rules). Of course, the AI could invent an ad hoc logic language and write a prover for it, but in this thought exercise, I think the point is that people would want to verify the proven properties (and possibly the implementation of the proof checker).

> What’s easier: verifying the high-level matrix multiply to machine code lowering is correct (per machine) and therefore every application of it is correct; or that every single bespoke matrix multiply actually correctly implements matrix multiply for every machine?

This isn't too relevant. If you need to build a skyscraper for tens of millions of dollars, you wouldn't spend much time thinking about how to lower the cost of the handle on the front entrance by $10. Even if every matrix multiplication is a little different, the proofs can be copied and changed slightly. The difference in cost of doing that or not is negligible compared to other aspects of the verification. Again, we write programs that are three orders of magnitude larger than the largest program we've ever managed to prove correct, and the difficulty does not scale linearly. So we're talking about an AI that's 10,000 or 100,000 times more capable than humans at writing software. Surely, matters as duplicating code and proofs are negligible for it.

But even if it does matter, machine code isn't a problem because you don't have to duplicate manually. You can write the machine code that specialises the different applications and prove the correctness of that. This is like writing a small portion of a compiler.

My general point is that proving arbitrary (practical) correctness properties of arbitrary (practical) programs is such a monumental achievement that anything more mundane, like a compiler, is trivial in comparison. It's like saying that someone can boil an ocean or move a mountain, but we must order them a taxi to get there.

It needs a special language for both. Machine code is a special language for programming, and since this is an exercise in imagining what an AI that could do anything would do, I don't see why it would need anything else. Machine code, however, follows the rules of a computer and not of those of a predicate logic, hence another language is needed for proofs.

I've done my share of formal verification (see my old blog in my profile) and of programming in Assembly, and obviously the former is far harder than the latter. People have only managed to formally prove the correctness of programs (end-to-end) under ~10 KLOC. If for some reason an AI capable of writing and proving arbitrary programs thinks it will be aided by a compiler, surely it will be able to create its own ad-hoc one for the problem at hand.

We used to write programs without a compiler. We'd write them in Assembly. The AI won't even need the assembler. If verification is done through formal proofs, a logic language is, indeed, needed, but the program itself could remain in machine code.

Yes, but also, who do you gather requirements from? Other people. But if we're talking AGI, then these other people, i.e. users - or at least those who define the requirements - could be replaced, too.