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.

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?

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.

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.

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

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

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.

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.

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.