3 ms·
What 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 sym
by simias 5y ago
What 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.