The annotations look pretty complex. It’s a whole other type language grafted on to C, and at least to me, even with the explanation in the introduction, very difficult to get an intuition of.

It reminds me of Google’s closure compiler-annotated JavaScript, where the ES4 type system was encoded in comments around the code. That was pretty frustrating to use, and switching to TypeScript where the types are actually part of the language was a significant improvement.

I suppose the benefit here is that you can annotate existing C code without re-writing it in a new language. Although I didn’t read enough to find out how well the refinement language can describe existing C coding patterns, which may not be provably safe. Similar to how type-safe JavaScript has to eschew certain control flows and meta programming, or null-safe Java has to conform to a certain style of programming to satisfy the null ness checker.

I salute the idea of fixing C shortcomings instead of starting over from scratch (Rust, Zig), but clearly this mix of large functional annotations on top of procedural code adds some burden and inelegance.

The automated formal code proving will appeal security researchers, but I doubt most developers will want to go through that.

As a developer, I would rather use checked-C since it's only a thin overlay requiring little syntactic sugar on top of C99. https://github.com/microsoft/checkedc

However, unlike RefinedC, it requires a new compiler and headers...