3 ms·

> Then of course there's language choice. C is king, which isn't necessarily a bad thing, but it's certainly not the safest, even in the restricted forms used i

by CHY872 11y ago

> Then of course there's language choice. C is king, which isn't necessarily a bad thing, but it's certainly not the safest, even in the restricted forms used in avionics. Sadly, my very first ever project as a programmer was porting an Ada codebase to C for the 787 (off by one errors for days...). It's almost cliche to say nowadays, but I would be really excited to see Rust gain some traction in avionics over the next 20 years or so. Because that's how far behind avionics is. We were using Visual Studio 6 in 2011! C has the big advantage that having been used for many years, it is very well understood, the compilers that exist are mature, and the formal analysis tools you want to use in a high assurance setting all exist also. Higher level languages usually have none of these things.

deleted 11y ago
[deleted]
randomsearch 11y ago
> C has the big advantage that having been used for many years, it is very well understood, C is probably the least understood language I know of. Vast parts of it are undefined, everyone makes their own decisions and compiler writers define the language. C is a practical choice because it is performant, legacy code exists, and because a lot of people know the language. Personally, I would never take a job writing safety-critical code in C. To give a single example of a far superior language for such applications, I would consider SPARK Ada, amongst others. I don't know how people that work on safety critical systems using C can sleep at night. C is for systems programming where performance is king, not for building software that can kill people.
- CHY872 11y ago
  Ada is a good decision in this field. Nevertheless, the parent was comparing C to Rust, where the language is immature, has no static analysis tools (to pick up the most important bugs), no well defined semantics and is entirely unproven in the field. This is the barrier for entry.
  - kibwen 11y ago
    Rust's compiler is itself a static analysis tool that is more powerful than any static analysis that can be written for C. There is also a blossoming collection of "lint" libraries that extend Rust's type system to provide user-defined static analysis passes. Servo uses lints like these extensively to help manage interaction with SpiderMonkey, whose (C++-based) garbage collector manages the nodes in Servo's (Rust-based) DOM. It's absolutely true that Rust is yet to be proven. We need to be ever careful not to oversell its benefits. But here's something that's been proven time and time again: use of C is fraught with horrors and pitfalls, and we should all be frantically seeking to improve the situation; if not via Rust, then via something else.
    - CHY872 11y ago
      You could do with some learning about what's possible with static analysis. For example, will the Rust compiler prove that your program must follow some state machine? (SLAM2). Will it compute a useful upper bound on the stack usage for your program? (a3/stack) Will it compute a useful upper bound on the runtime of your program? (a3/WCET) Can one prove (in certain cases) zero potential execution errors? (Astré)? Can one automatically prove generic first order logical specifications of a program? (Caveat) A lot of these are decades old theory that have been put into practice that simply don't work in the context of a compiler. I'm sure they could be made to work with Rust, but they haven't. You can do a lot more with static analysis with time and money than you would want to do in a compiler for a language that's a couple of years old. Furthermore trusting Rust's statically derived guarantees means trusting the Rust compiler to have no bugs. One does not need such a leap of faith for C; they can use a formally verified compiler: http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris... Writing a formally verified compiler for Rust would be (I'm sure of this) a right pain in the arse.
      - CHY872 11y ago
        Sorry, that came off overly harsh, I think. Anyway, static analysis is really cool :)

by CHY872 11y ago

deleted 11y ago

[deleted]

randomsearch 11y ago

> C has the big advantage that having been used for many years, it is very well understood, C is probably the least understood language I know of. Vast parts of it are undefined, everyone makes their own decisions and compiler writers define the language. C is a practical choice because it is performant, legacy code exists, and because a lot of people know the language. Personally, I would never take a job writing safety-critical code in C. To give a single example of a far superior language for such applications, I would consider SPARK Ada, amongst others. I don't know how people that work on safety critical systems using C can sleep at night. C is for systems programming where performance is king, not for building software that can kill people.

CHY872 11y ago
Ada is a good decision in this field. Nevertheless, the parent was comparing C to Rust, where the language is immature, has no static analysis tools (to pick up the most important bugs), no well defined semantics and is entirely unproven in the field. This is the barrier for entry.
- kibwen 11y ago
  Rust's compiler is itself a static analysis tool that is more powerful than any static analysis that can be written for C. There is also a blossoming collection of "lint" libraries that extend Rust's type system to provide user-defined static analysis passes. Servo uses lints like these extensively to help manage interaction with SpiderMonkey, whose (C++-based) garbage collector manages the nodes in Servo's (Rust-based) DOM. It's absolutely true that Rust is yet to be proven. We need to be ever careful not to oversell its benefits. But here's something that's been proven time and time again: use of C is fraught with horrors and pitfalls, and we should all be frantically seeking to improve the situation; if not via Rust, then via something else.
  - CHY872 11y ago
    You could do with some learning about what's possible with static analysis. For example, will the Rust compiler prove that your program must follow some state machine? (SLAM2). Will it compute a useful upper bound on the stack usage for your program? (a3/stack) Will it compute a useful upper bound on the runtime of your program? (a3/WCET) Can one prove (in certain cases) zero potential execution errors? (Astré)? Can one automatically prove generic first order logical specifications of a program? (Caveat) A lot of these are decades old theory that have been put into practice that simply don't work in the context of a compiler. I'm sure they could be made to work with Rust, but they haven't. You can do a lot more with static analysis with time and money than you would want to do in a compiler for a language that's a couple of years old. Furthermore trusting Rust's statically derived guarantees means trusting the Rust compiler to have no bugs. One does not need such a leap of faith for C; they can use a formally verified compiler: http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris... Writing a formally verified compiler for Rust would be (I'm sure of this) a right pain in the arse.
    - CHY872 11y ago
      Sorry, that came off overly harsh, I think. Anyway, static analysis is really cool :)