This is just something I've been thinking about. My experience is that agents aren't useful if you view them as programmers, because you still have to audit all the code until we get to the point where you don't, which may be quite far off.But if you view them as a replacement/driver for the Unix shell, as much as I have loved it for many years, it does seem like you can move faster.
LLMs may theoretically be able to generate millions of correct lines of code.But for any important code the only way to know that it's correct is to hand-audit every line, which is harder than writing every line because this allows you to build a conceptual hierarchy and model within which you can think about the code.So there's a fundamental limit to the speedup from LLMs when writing anything...
Call me a snowflake, but 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.subligence /sʌbˈlɪdʒəns/ n.A lesser or rudimentary form of intelligence; the capacity to respond, select, or adapt without full understanding. The semblance of mind in...
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.
Hi HN,We're working on Xr0 [0] and have been building a static-site generator that meets our tastes and needs. The basic emphasis is on simplicity and content rather than customisability and feature-richness. We are imitating Jekyll and Hugo (and other SSGs) in their basic generation paradigm and LaTeX in its separating form from content, but attempting to combine these into a unified, minimal...
if (x > 0) {
/* code */
} else {
/* more code */
}
Xr0 is a work in progress, and we'll get there step-by-step.
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`.
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...
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])
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'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.
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.
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.
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#...
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.