2 ms·

Sure. I'm also a big fan of what Microsoft has done with SAL. And of course you have formally proven C, as used in seL4. I'd say that the contortions you have t

Sure. I'm also a big fan of what Microsoft has done with SAL. And of course you have formally proven C, as used in seL4. I'd say that the contortions you have to go through to write code with these systems takes you out of the domain of "C" and into a domain of a different, safer language merely resembling C. Such a language might be a fine tool! But it's not arbitrary C.

uecker 2y ago
Note that my original comment above was "reasonably safe" and not "perfectly memory safe". You can formally prove something with a lot of effort, but you can also come reasonably close for practical purposes with a lot less effort and more commonly available tools. You are right that "arbitrary C" is not safe while safe Rust is safe, but this is mostly begging the question. The question is what can you do with the language depending on your requirements. If you need safe C this doable with enough effort, if you need reasonably safe C this is even practical in most projects, and all this should be compared to Rust as used in a similar situation which very well may include use of unsafe Rust or C libraries which may also limit the safety.
ryao 2y ago
It is C. It is just written with the aid of formal methods. It would be nice if all software were written that way. That said, if you want another language “resembling C”, there is always WUFFS: https://github.com/google/wuffs https://github.com/google/wuffs The output of the WUFFS compiler certainly resembles C because it is C.
- lmm 2y ago
  > It is C. It is just written with the aid of formal methods. It is not C in the sense that many of the usual reasons to use C no longer apply. E.g. a common reason to use C is the availability of libraries, but most popular libraries will not pass that analyser so you can't use them if you're depending on that analyser. E.g. a common reason to use C is standard tooling for e.g. automated refactoring, but will those standard tools preserve analyser-passing? Probably not.

uecker 2y ago

Note that my original comment above was "reasonably safe" and not "perfectly memory safe". You can formally prove something with a lot of effort, but you can also come reasonably close for practical purposes with a lot less effort and more commonly available tools. You are right that "arbitrary C" is not safe while safe Rust is safe, but this is mostly begging the question. The question is what can you do with the language depending on your requirements. If you need safe C this doable with enough effort, if you need reasonably safe C this is even practical in most projects, and all this should be compared to Rust as used in a similar situation which very well may include use of unsafe Rust or C libraries which may also limit the safety.

ryao 2y ago

It is C. It is just written with the aid of formal methods. It would be nice if all software were written that way. That said, if you want another language “resembling C”, there is always WUFFS: https://github.com/google/wuffs https://github.com/google/wuffs The output of the WUFFS compiler certainly resembles C because it is C.

lmm 2y ago
> It is C. It is just written with the aid of formal methods. It is not C in the sense that many of the usual reasons to use C no longer apply. E.g. a common reason to use C is the availability of libraries, but most popular libraries will not pass that analyser so you can't use them if you're depending on that analyser. E.g. a common reason to use C is standard tooling for e.g. automated refactoring, but will those standard tools preserve analyser-passing? Probably not.