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