3 ms·

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 u

by 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 :)
    - kibwen 11y ago
      NBD, I was being a little overzealous there myself. :) IME when most people say "static analysis" they're referring to tools that attempt to detect the usual class of memory vulnerabilities that Rust prevents outright (or maybe they do even worse and just attempt to detect typical coding patterns which happen to be correlated with the same). Part of my zeal is also that Rust's semantics are strictly, er, stricter than C's (disregarding the quagmire of C's undefined behavior), which means that static analysis tools should be even easier to write for it.

by CHY872 11y ago

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 :)
  - kibwen 11y ago
    NBD, I was being a little overzealous there myself. :) IME when most people say "static analysis" they're referring to tools that attempt to detect the usual class of memory vulnerabilities that Rust prevents outright (or maybe they do even worse and just attempt to detect typical coding patterns which happen to be correlated with the same). Part of my zeal is also that Rust's semantics are strictly, er, stricter than C's (disregarding the quagmire of C's undefined behavior), which means that static analysis tools should be even easier to write for it.