4 ms·
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
by wffurr 5y ago
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.
- rahen 5y ago> 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...
- sanxiyn 5y agoWhen you say "may not be provably safe", do you mean 1) it is safe but hard to prove, or 2) it is not safe? RefinedC is sound, so it can't handle 2. For 1, while it focuses on automation, it has an escape hatch with which you can use full prover, so it should be able to handle anything that is actually provable.
- wffurr 5y agoI meant 1). Drawing by example from TypeScript and Java nullness checkers, certain programming idioms are fine in practice and programmers can reason about them, but they're difficult to express in a provable way. Sometimes it's limitations in the tools; other times it's actually unsafe but safe in practice due to an invariant maintained elsewhere but not actually expressed in the code under consideration.
- simias 5y agoWhat I find even more perplexing is that they decided to add new syntax for these annotations but still decided to stuff them into strings and add non-ascii symbols into them: [[rc::constraints("{s = {[n]} ⊎ tail}", "{∀ k, k ∈ tail → n ≤ k}")]] APL meets GCC inline assembly syntax. A dream come true. At this point I wonder if it would be much more trouble to just port the code to Rust.
- zozbot234 5y agoThis looks like they just embedded Coq syntax directly, so using strings is quite normal.
- simias 5y agoI didn't realize that this was Coq, that makes more sense. Still, if this is meant to be used by C coders it might be worth stooping to our level, many of us won't be comfortable with this mathematical notation. I know I'm not, and I know I'm not the most mathematically illiterate in general.
- sanxiyn 5y agoThis is not meant to be used by C coders, at least not yet. The thing is, experts struggle to verify C. This is an aid to experts so that C can be verified at all. Ease of use comes after that.