> 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

> 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. 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 https://github.com/microsoft/checkedc However, unlike RefinedC, it requires a new compiler and headers...