Xr0 verifier, guarantee the safety of C programs at compile time

Previously:

Show HN: Xr0 – Vanilla C Made Safe with Annotations (https://news.ycombinator.com/item?id=37536186, 2023-09-16, 13 comments)

Xr0 Makes C Safer than Rust (https://news.ycombinator.com/item?id=39858240, 2024-03-28, 41 comments)

Xr0: C but Safe (https://news.ycombinator.com/item?id=39936291, 2024-04-04, 144 comments)

Show HN: Xr0 is a Static Debugger for C (https://news.ycombinator.com/item?id=40472051, 2024-05-05, 4 comments)

Cute. They've introduced ownership to C. The annotation system is expressing ownership, in a rather clunky way. You have to explicitly declare that functions create or release allocated space. That's ownership tracking.

But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem.

From the tutorial:

    #include <stdio.h>
    int main()
    {
        int i;
        return i;
    }
    the behaviour is undefined because i’s value is indeterminate.

That was in the first version of D because I have spent days tracking down an erratic bug that turned out to be an uninitialized variable.

I don't see any explanation of what niche this targets relative to pre-existing tools like Checked C, CMBC, or Frama C...

What happens if a function allocates not deterministically, like

if (turing_machine_halts(tm)) return malloc(1); else return NULL;

How is this handled?

Does it require annotations or can it validate any c code?

It's odd that so many people promote rust, yet we don't even use static analysis and validators for c or C++.

How about enforcing coding standards automatically first, before switching to a new language?