akiarie

Never mind, someone else already made this point: https://electric.ax/blog/2026/02/19/amdahls-law-for-ai-agent...

True, but thing is that "artificial intelligence" is meant in the opposite sense. It's meant as something that is / will be equivalent to human intelligence, not as something useful but vastly inferior.

I propose that those of us who don't believe that AI is actually intelligence look for a term to refer to its "thinking" that isn't "intelligence", because this helps our weak minds keep things straight.

C is still, by far, the simplest language that we have.

Although many newer languages are safer (with the exclusion of Rust, primarily by being slower) the same kinds of issues that are there in C are there in these languages, their effects are just harder to see.

People complain about C as though they know how to fix it.

"Verbose" is the wrong adjective. Yours is a terse projection into a lower space, valid in itself, but lacking the power and precision of its archetype.

This is such a beautiful distillation of everything I believe about the dangers of over-reliance on AI. I implore thee, good sir, to write a longer essay on this.

Obviously because he was one of the architects of the censorship regime of the late 2010s and early 2020s that nearly changed the internet into a three-letter-agency controlled space. If that isn't a risk for a censorship-resistant app, I don't know what is.

Not even remotely.

  if (x > 0) {
    /* code */
  } else {
    /* more code */
  }

0db is an interface for Xr0, so it's the same thing essentially.

Shouldn't it be called "We can't parse C" since we can only parse a trivial subset of it?

It's even less impressive than that. That we can parse a subset of C. That's all there is to see here.

You missed the `!=`, `==` (in many instances), bitwise operators, recursion and `goto`. (And much, much more.)

Xr0 is a work in progress, and we'll get there step-by-step.

It really isn't. The second example is ...

So will you admit that the first example has been sufficiently addressed? Because I was commenting on the problem involving the Collatz conjecture.

It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.

True. As you said earlier:

The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.

This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.

It's because we're dealing with an extreme example in which a program's safety depends on the resolution of an open problem.

If the program's safety depends on the semantics of C and how they've been used in a function, it will be possible to deal with all the conditions upon which a program could be unsafe (in the sense of the standard safety vulnerabilities – like those listed here [0]). Doing so would lead to denouement, so that the annotation to the main function would be empty (meaning none of those bugs can occur).

Programs that might be unsafe should not be verifiable.

[0] https://alexgaynor.net/2020/may/27/science-on-memory-unsafet...

Thought provoking stuff! I really appreciate how much effort you've put into this.

However, the main reason why this argument is flawed is it omits the heart of the matter: the annotations. Xr0 empowers programmers to propagate safety semantics. A program that is only safe if the Collatz conjecture holds is (surprise) only safe if the Collatz conjecture holds. So in Xr0 the only requirement we would impose is that this program be augmented with an annotation that communicates that it is only safe if the Collatz conjecture is true.

So the flaw in the reasoning is we haven't claimed that Xr0 can prove arbitrary programs are safe. We've claimed that Xr0 can prove the correspondence between the safety semantics denoted in an annotation and a function body. Above there are no annotations given which would specify "this program is safe only if the Collatz conjecture is true". It shouldn't be hard to prove the correspondence between such an annotation and the program you've written, e.g.:

    def main(): ~ [
        buffer = [0, 0, 0, 0, 0]
        x = int(input())
        if x >= 1:
            collatz_cycle_element = cycle(collatz, x)
            print(buffer[collatz_cycle_element])
    ]

        buffer = [0, 0, 0, 0, 0]
        x = int(input())
        if x >= 1:
            collatz_cycle_element = cycle(collatz, x)
            print(buffer[collatz_cycle_element])

Xr0 1.0.0 will enable programming in C with no undefined behaviour, but for now it's useful for verifying sections of programs.

Literally on the website. The purpose of the prototype is to show the feasibility of the approach we've taken, not to work on whole programs.

You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works.

You're right. We should. (We will be adding this as we are able.)

You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.

A 7-point blog post is hardly "long-form" :)

But more to the point, Rust has already achieved this "interface formality", as we state in the second paragraph of this "long-form" piece. That achievement on the part of Rust is indeed groundbreaking. Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality?

Fair enough. We have a much more generous definition of "working prototype" than you do. Hopefully one day soon we'll have something that clears yours.

One final point – I cannot emphasise strongly enough that we aren't making this for Rust programmers. There's nothing wrong with loving a programming language that has changed the world and what is possible in systems programming. Rust is an advance for systems programming, and it's made incredible strides.

But some programmers (like myself) love working in C, and do not like Rust's restrictions. For such programmers even if the question was one of re-implementation (which we don't think it is) Rust would remain undesirable.

If annotations aren't copies of function bodies (which is really the only sensible choice), you need to deduce whether a function body matches the annotations. "Structural similarity" between C and your annotation syntax won't make this easier. In fact, it is impossible to deduce whether two C functions are semantically equivalent even though C is extremely structurally similar to C (you could even argue that C and C are structurally identical).

Maybe I don't understand your point. I am not denying that we're deducing that the body matches the annotations. I'm simply saying that for the restricted case of safety semantics alone, this deduction can be done. Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body. If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.

So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".

Your quote omits the first sentence of the paragraph, which states that "well-designed programs exhibit [denouement] very strongly". Denouement in the sense we're referring to is an absolute theoretical necessity for any safe program, because at some level (of functional abstraction) the safety concerns must be handled, otherwise the program would have a safety vulnerability.

Xr0 definitely limits constructs, but our claim is that the limitation we're imposing is one that reflects the structure of all safe programs. The same cannot be said about Rust's ownership semantics, which limit an enormous number of simple, safe constructs. So the C programs to which one would be adding Xr0 annotations wouldn't need to be rewritten unless a bug has been discovered.

Even on this small subset of C it took me five minutes to get an out of memory error and a further five minutes to craft a C program with a double free that passes verification [10].

Nice work with the program. However, the only reason it verifies is we haven't yet implemented `||`, so in the parser the phrase `if (x || !y)` is being interpreted as `if (x)` (see [0] for the relevant production). This may seem like another frustrating indiction of how "extremely limited" the subset of C that Xr0 works on is, and indeed it is. But the most important point is there is no logical flaw in Xr0's design here, and no reason whatever that an error of this kind wouldn't be detected. [1] is an equivalent program that shows the logical cogency of our approach (I know it's ugly!).

I'm doubtful Xr0 will be useful for someone without a background in formal verification.

Most of the people interested in formally verifying their C code will already know about formal verification and absolutely don't care about whether Xr0 is written in C or not.

We aren't making Xr0 for people (self-consciously) interested in formal verification, but for C programmers interested in safety of the kind that Rust provides. And I can tell you that C programmers prefer their tools in C.

All this combined with a website that makes great promises about how awesome Xr0 is (or rather going to be) and handwavy explanations about how easy adding the missing features will be that don't hold up to any scrutiny. Dozens of similar projects exist, few of them work at all on non-trivial C programs and all of them require herculean effort (and are thus only used for safety critical software) to correctly annotate C code (often this includes rewriting parts of the code to make the annotations simpler or unnecessary). There is no discussion at all how Xr0 is going to solve the problems that killed these projects.

Fair enough. The proof is in the pudding. Give us a few months. But understand that we have limited resources (this is an open source project and we're working on it part-time). We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.

[0] https://git.sr.ht/~lbnz/xr0/tree/master/item/src/ast/gram.y#...

[1] https://pastebin.com/raw/7EpcUVzv

If the annotation is basically just a copy of the function body why have any annotation at all?

This is a profound question. Xr0 annotations seem to be copies of the function bodies, but they aren't actually. What they are is a description of the function's safety semantics, the side effects and circumstances under which the function may be relied upon to exhibit well-defined behaviour (under the C Standard).

They only seem to be copies of the bodies because we're dealing with simple examples in the post here and in the tutorial, but we have a much more significant program ready (documenting) that we'll be sharing soon that shows the difference more clearly.

Xr0 is built in explicit reliance upon the powers of programmers to structure code in such a way that the annotations become simpler and simpler as you move up layers of function abstraction. As a simple example, think about what happens when you allocate memory and free it within a function, e.g.

        #include <stdlib.h>

        void
        foo() ~ [ return malloc(1); ]
        {
                return malloc(1);
        }

        void
        bar()
        {
                void *p = foo();
                free(p);
        }

        void
        baz()
        {
                bar(); /* completely safe */
        }

We call this simplifying phenomenon denouement, and well-designed programs exhibit it very strongly. Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0.

It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.

Yes, but we don't. Only well-defined behaviour according to the C Standard. This is the goal for Xr0 v1.0.0. After that the sky is the limit.

Rust's restrictions can also be interpreted as restrictions on interfaces. A function taking (a non-`Copy` type) by value is a function that Xr0 would annotate as `free`ing that variable, for example.

Yes they can, and we said this in the article, "The remarkable safety guarantees that Rust provides are consequent to something much deeper than its ownership rules: Rust empowers programmers to formalise and verify the semantics of pointer usage at the interface boundary between functions. If interface formality is the fundamental determinant of safety, systems language design should focus directly on it rather than on any other criterion, including ownership."

The point we're stressing, though, is that the restrictions in Rust do not focus on the interfaces, but on the ownership principle. So we're advocating for language design to ignore ownership considerations and deal with the interfaces as the important point.

You are claiming that Xr0 will deduce that a function matches its annotations. If those annotations are "this function has property P", you'll have to deduce whether the function actually has property P. This can be augmented by inline annotations (i.e. annotations for code, not interfaces) and those will likely become necessary once you implement loops. But at that point you'll have reinvented Frama-C and you'll realize why Frama-C isn't used outside of safety-critical software: It's both hard and exhausting to use.

Again, I agree with most of this (except the cynicism). We have done some serious experiments with implementing loops and immediately saw that we would need to annotate the loops also (with at least some kind of invariants).

The comparison to Rust is actually a whole lot more helpful than that to Frama-C. Why is Rust able to deliver safety guarantees without becoming "hard and exhausting"? Our argument is that it is the interface formality issue that really determines safety. If this is so, why should it be "hard and exhausting" to be empowered with the ability to be formal at the interfaces concerning the things that influence safety?

The fact that we're using annotations does not mean that Xr0 is equivalent to Frama-C. To point to one important difference, we're focused on securing safety, whereas Frama-C is a general purpose tool for arbitrary correctness considerations. If Xr0 does grow to deal with such arbitrary correctness concerns, it is possible that it will become "hard and exhausting" like Frama-C, because of the inherent difficulty of complete verification. But while we're focused on safety alone, there's no reason why we can't offer something that is at most of the same difficulty level of working in Rust. Xr0's annotations are not "this function has property P" where P is arbitrary. They are "this function has well-defined behaviour according to the C standard under these circumstances". That is a much more limited kind of condition to validate.

I'm not very familiar with the equivalence problem, but at least for Xr0 abstracts (what we call the annotations attached to functions & loops) there is an extremely strong structural similarity between the implementation and the annotation. So it's not at all clear that we'll run into this.

The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation?

This is a pivotal question and our answer to it exposes one of our basic assumptions. Interfaces do hide underlying complexity, but that is not all that they do. They define our interaction with abstractions, which not only hide complexity, but reduce it by "abstracting". So what we find in practice is that the interfaces are not as complicated as the code, because all they define is what the higher levels of abstraction need to know to interact abstractly with the lower levels.

One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort.

Well this is great. If you like Rust, there's nothing wrong with that. But many C programmers don't feel this way.

Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail.

Insightful again! This is all true. Note, however, that we aren't claiming not to impose restrictions. We're claiming that the restrictions should concentrate at a different place than where they concentrate in Rust. They should orbit around the interfaces. Xr0 is certainly imposing restrictions there.

Moreover, we are in no way suggesting/claiming that we can deduce the safety of arbitrary C programs, which is the whole reason the annotations are required. We're claiming that we can help programmers who already understand why their code is safe express these reasons in relatively-simple annotations, and use these to verify their reasoning.

Edit: typo.

I don't think you're under any obligation, I just think that not discussing prior art is a bad look.

See [0] where our reliance on Dijkstra is transparent.

I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche.

Begin with the fact that Xr0 is written in C and feels like C. We're building it so that C programmers will be able to use it without explicitly learning about formal verification.

Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.

Absolutely true. But what I mean by "mathematician" is a self-conscious mathematician, or at least someone with a background in formal mathematics.

(Edit: forgot to add link.)

[0] https://xr0.dev/dijkstra-paradox

It cannot in general deduce the abstract. Doing so would require solving the halting problem.

"Simpler" is the word that we care about. Although Rust is an advance on C in many significant ways, what it loses is the simplicity. One of our goals is to offer three same advances (and more) but without compromising on simplicity.

Interesting points. Because it's easy to do the type checking at compile time for function prototypes (though we haven't implemented it yet) we haven't felt under pressure to use the `func(void)` notation, which has always felt somewhat uncouth to me.

The verbosity of the annotations is the most jarring thing at the beginning. However, do you find any of them unclear? Because we're optimising for similarity to C before terseness.

Since we are not academics, I don't see why we're under obligation to do a comprehensive literature review, especially early on. We aren't claiming to have invented these techniques. It should be obvious that Xr0 involves very little in the way of new ideas. Our primary reference has been the work of Dijkstra.

What is significant about Xr0 is how it applies these old ideas. Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.

Yes, the code example you've given is exactly in the direction we're thinking. (Edit: thought it can't be verified yet.)

We haven't documented the algorithm because it's not the unique part of what we're doing. It works in a very simple-minded way, analysing possible states.

The interesting part is the insight that function interfaces are the boundary along which verification should take place. Applying this idea consistently we escape the combinatorial explosion which tends to plague efforts in this area, because every function can be verified by itself. Notably, Dafny recognised this point before us, and the earliest clear statement we can find regarding it is in Dijkstra's "Notes on Structured Programming", in his chapter "On a Program Model". You may find that illuminating read.

I'm no expert on Clang/GCC and the new annotation syntax for C and C++, but from what I've seen it's not general enough for what we're trying to achieve in Xr0. The safety semantics which are expressed in annotations in Xr0 (see [0] for an example) get very detailed.

[0] https://xr0.dev/learn#initialisation-of-memory-and-the-clump