[wuschel]

From a C-veteran perspective, what do you think about type safe (e.g. dependent types such in ATS, or F*/KreMLin, or other DSLs) languages that compile to C, or a subset of C?

How could one get the safety promises that are observed in Rust in C?

Thanks!

[ajxs]

I'm not the OP you're asking, I'll provide my own answer to the latter question though.

C is a language that doesn't come with many guarantees. I personally like to think of C as a 'higher-level assembler', targeting a virtual machine. I've been led to believe that this figurative description of the language was more common in the past than it is today. I find it a helpful description since it offers an explanation for many of C's design choices. Such as it's weak types and use of pointers. If I'm correct it's also an accurate description of the language's original aims in system development.

Also, Rust isn't the only systems programming language with a focus on safety. Ada has been around for some time now and is a much more mature language and arguably more suited for the job. It has a demonstrable track record of successful use in safety-critical software. Rust is definitely more 'C-like' than Ada, which might make it preferable to many.

[wuschel]

I see. Thank you very much for your explanation.

I always thought that after so many years, there must be a testing framework, development tools and methodology to give a C developer the safety that his problem requires. What do people use when they are programming critical systems e.g. defense,health,flight control, etc. Problems like Heartbleed et al are not something that can be ignored in the industry.

That is why I wondered about advanced tools I heard about e.g. ATS, Compcert, and so on. As I understand, the model that is used in Rust comes with limitations in regard to program design.