3 ms·

Previously: Show HN: Xr0 – Vanilla C Made Safe with Annotations (https://news.ycombinator.com/item?id=37536186 https://news.ycombinator.com/item?id=37536186, 2

Previously: Show HN: Xr0 – Vanilla C Made Safe with Annotations (https://news.ycombinator.com/item?id=37536186 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 https://news.ycombinator.com/item?id=39858240, 2024-03-28, 41 comments) Xr0: C but Safe (https://news.ycombinator.com/item?id=39936291 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 https://news.ycombinator.com/item?id=40472051, 2024-05-05, 4 comments)

tialaramex 10mo ago
Thanks! I thought this felt familiar. 2023 is a long time to still be in this "Initial signs are promising" mode. There are no code commits since March 2025. I've had projects which stalled for a few months or even a year, but generally if I said I'll get to it "soon" and two years later I haven't, that's not getting done. There are two boxes of books I planned to unbox "soon" after discovering that the bookshelves for my new flat were full & so I had nowhere to put them. That was when Obama was still President of the United States of America. Don't expect me to ever get around to unboxing those books, I clearly haven't even missed them.
- muldvarp 10mo ago
  The initial sign for Xr0 never seemed promising for anyone with experience in formal verification. Neither the code nor the ideas they presented were new. I asked them multiple times to clarify how their project differed from the dozens of already existing options for formal verfication of C programs and never got a concrete answer.
  - tgv 10mo ago
    As I see it: tracking (de)allocation in a very simple, understandable way. Unfortunately, that seems to be all it does. It's a start, certainly if you don't want to/cannot use a more complete system, since they can be quite complex. I'm not following this space professionally, only out of interest a bit, but do you know of a system that is so simple?
    - muldvarp 10mo ago
      Xr0 isn't any simpler than for example Frama-C. In fact one of the simplest (but still useful) systems for statically tracking ownership is Rusts borrow checker, which the authors of Xr0 say is _too_ simple.
- rurban 10mo ago
  Well, apparently someone rewrote it in rust, which was better than their version. Which they needed some time to process how to continue. And they got stuck with the bounds checker and loops. But other such checkers are far more advanced, with a better contract syntax.

tialaramex 10mo ago

Thanks! I thought this felt familiar. 2023 is a long time to still be in this "Initial signs are promising" mode. There are no code commits since March 2025. I've had projects which stalled for a few months or even a year, but generally if I said I'll get to it "soon" and two years later I haven't, that's not getting done. There are two boxes of books I planned to unbox "soon" after discovering that the bookshelves for my new flat were full & so I had nowhere to put them. That was when Obama was still President of the United States of America. Don't expect me to ever get around to unboxing those books, I clearly haven't even missed them.

muldvarp 10mo ago
The initial sign for Xr0 never seemed promising for anyone with experience in formal verification. Neither the code nor the ideas they presented were new. I asked them multiple times to clarify how their project differed from the dozens of already existing options for formal verfication of C programs and never got a concrete answer.
- tgv 10mo ago
  As I see it: tracking (de)allocation in a very simple, understandable way. Unfortunately, that seems to be all it does. It's a start, certainly if you don't want to/cannot use a more complete system, since they can be quite complex. I'm not following this space professionally, only out of interest a bit, but do you know of a system that is so simple?
  - muldvarp 10mo ago
    Xr0 isn't any simpler than for example Frama-C. In fact one of the simplest (but still useful) systems for statically tracking ownership is Rusts borrow checker, which the authors of Xr0 say is _too_ simple.
rurban 10mo ago
Well, apparently someone rewrote it in rust, which was better than their version. Which they needed some time to process how to continue. And they got stuck with the bounds checker and loops. But other such checkers are far more advanced, with a better contract syntax.