Syntax appears to be incompatible with C

[nonnull-ca]

The webpage starts with "Xr0 is a tool for proving that C programs are safe at compile time.". Which is great, and a laudable goal.

Only... the actual code example does not appear to be valid C.

/* the [] part tells Xr0 we're using the heap */
void *
alloc1() [ .alloc result; ]
{
    return malloc(1);
}

[ .alloc result; ] in particular is not allowed by any edition of the C specification I know of, nor accepted in practice by either GCC or clang. It is close, but not identical to (nor compatible with) the C23 attribute syntax. (As an aside: I do not suggest adopting the C23 attribute syntax directly. There are too many programs that would benefit from static analysis tooling that are currently on older versions of the C standard, and incrementally adding annotations is far less of an ask than upgrading the codebase wholesale.)

If this is not intended to prove that (a subset of) C programs are safe at compile time, and is instead intended to prove that programs in a C-like language are safe at compile time, could this please be better-documented? (This would still be unfortunate, and a non-starter for any programs that wished to be compatible with multiple C compilers.)

Alternatively, could the annotation syntax be changed to something that is valid C, such as specially-formatted comments, or tokens that can be #define'd out of existence on other compilers?

[akiarie]

This question cuts to the heart of our design concerns. Let me try and break down our thinking around it.

The actual code example does not appear to be valid C.

We say that Xr0 is C because all that Xr0's annotations do is express C's safety semantics as they are. Xr0 allows C programmers to express and verify the safety properties of their C code. The semantic annotations are completely orthogonal in effect to the code that is presented to the C compiler and the machine. The point of contrast is an additive language (like the original C++) which compiles to C, but is meant to enable programmers to operate "above C". With an additive language, you could never subtract the added parts of the program, but in Xr0 the subtraction is part of the design. So while it is true that the source file is not C (which we admit by introducing *.x files), the language in which one has to operate to use Xr0 is C. Xr0 exists to support C as it is, not to transcend it. It is a servant, not a descendant, of C.

Alternatively, could the annotation syntax be changed to something that is valid C, such as specially-formatted comments, or tokens that can be #define'd out of existence on other compilers?

This point is about tradeoffs. Relegating the annotations to comments makes them more immediately compatible with C compilers, but it also relegates them to comments, making them second-class citizens. They will never feel native. Placing them in comments also means that they cannot have their own comments unless we introduce another comment sequence for the annotation environment. Again, it means that we can't use the preprocessor, so annotations for code with say, conditional compilation, become impossible. (The idea to use #define'd tokens for the annotation environment is good, but sadly only normal identifiers are allowed, so we would have to do something ugly like XR0_START and XR0_END.)

So basically, we're trading some compatibility for nicer, native-like source. For us, "beauty is the first test", and we believe that there's no way for the source to be beautiful if we put the annotations in comments.

[nonnull-ca]

Xr0 allows C programmers to express and verify the safety properties of their C code.

I may be missing something.

This appears to allow C programmers to express and verify the safety properties of newly-written code in a language that is incompatible with C.

It does not appear to allow C programmers to express and verify the safety properties of their C code - as, apparently by design, the resulting code is not valid C.

[akiarie]

I think this is an issue of definitions. The C standard defines a conforming implementation as any that "accepts any strictly conforming program", where a strictly conforming program is one that "shall only use those features of the language and the library specified in this Standard". It goes on to say

A conforming implementation may have extensions (including additional library functions), provided they do not alter the behavior of any strictly conforming program.

Xr0 is a conforming implementation of C in this sense. It will accept any strictly conforming C program and (leveraging existing compilers such as GCC and Clang) produce an executable for appropriate execution environments.

In addition to this, however, Xr0 will accept annotated programs, and it will use these annotations to give safety guarantees to its users. It will strip these annotations and produce executables correspondingly.

In this sense we believe that we are complying with the standard, and it would be misleading on our part to pretend we are making a new C-like language.

Hope this helps.

[nonnull-ca]

The Xr0 compiler appears to be a C-conforming compiler. I agree with you there.

Unfortunately, as far as I can tell the Xr0 compiler cannot be used for "proving that C programs are safe at compile time.'. It can be used for proving that Xr0 programs (as in, code that is written in the annotated form mentioned) are safe at compile time - but any such C code that has been ported to Xr0 is no longer spec-compliant C. (Aside from the trivial case of 'no annotations at all', of course - but that rather defeats the point.)

[akiarie]

The C program that Xr0 proves to be safe is not the Xr0 source file, but the C source that Xr0 will produce and pass off to GCC, Clang, etc. This program is pure C.

ION: GH will be functioning as a mirror for Xr0, but discussion will be on Zulip and mailing lists (which will be up soon). I'm closing this issue now but I will share it on Zulip and you can feel free to follow up from there. We'll be shutting down GH issues for the project in a couple of days.

Update: You can follow up from this thread on Zulip.