3 ms·

You can write reliable programs in C. How about a successful $2.5 billion mission to Mars with 500,000 lines of C? http://programmers.stackexchange.com/questi

You can write reliable programs in C. How about a successful $2.5 billion mission to Mars with 500,000 lines of C? http://programmers.stackexchange.com/questions/159637/what-is-the-mars-curiosity-rovers-software-built-in http://programmers.stackexchange.com/questions/159637/what-i... There are a lot of tools available for the design of reliable systems in C. Valgrind is just the beginning. A lot of smart people have put an enormous amount of effort into static and dynamic checkers and theorem provers, as well as standards and guidelines for what you need to do in order to write reliable systems in C. These systems have hard realtime and hard memory requirements. This is how it works at the extreme end of reliability requirements: you avoid Java and use C, because you'd have to validate the Java runtime anyway, much of which is written in C, and it's just plain easier to validate your C code under an otherwise crippling set of constraints. And then, as ill as you speak of C, you turn around and plug your Java systems into C systems, such as Varnish, Nginx, Apache, PostgreSQL, or thousands others that you use every day, not to mention the OS itself. Yes, I agree that it is crazy to write your web app in C. But web apps are not the entire world.

lmm 12y ago
At the point where you're using a theorem prover you're not really writing C any more (I mean, do you count ATS as writing C?). It's a perfectly good way to produce reliable code, sure. But I'm pretty sure it's not what the article is advocating. > And then, as ill as you speak of C, you turn around and plug your Java systems into C systems, such as Varnish, Nginx, Apache, PostgreSQL, or thousands others that you use every day, not to mention the OS itself. I do my best to minimize the C surface, and I worry about what I am exposing. E.g. I don't put Apache/Nginx/etc. anywhere in my stack (I either route directly to the JVM or use an Erlang load balancer), which means I wasn't running around patching them in the wake of Heartbleed. I'd use e.g. Riak over PostgreSQL wherever possible.
- spc476 12y ago
  Erlang is written in C, and the latest version is 456,000 lines of C. You might want to double think your reliance on such unstable technology.
- dietrichepp 12y ago
  I'm just taking two lines from the article: "Reliability and proven tools are even more important than libraries"... in this case, there are a lot of proven tools for writing C programs, including the theorem provers. And "You're more dependent on the decisions made by the language implementers than you think"... there have been a lot of flaws in the JRE over time, most of them from the parts of the JRE that are written in C. If you had been writing in C, you could have avoided those flaws if you were in the top 2% most diligent and careful C programmers, because the C tools are rock solid, whereas Java tools haven't been (January 2013 is still pretty recent). Problems in libraries, such as heartbleed, can be mitigated in C using the same tools that you'd use in Java. Process isolation is great. Of course, if you are writing your web app in C then I am going to replace you with someone else. But the web is not everything.
  - heinrich5991 12y ago
    What is such a theorem prover? I'm interested in it for trying to prove properties of my own programs...
  - lmm 12y ago
    The January 2013 flaws affected end users running the browser plugin, not systems written in Java. I suppose if you had a system that allowed users to submit their own bytecode and used Java's native facilities for handling this, then you'd be vulnerable. But nothing forces you to do that; someone who's capable of writing a safe bytecode verifier in C is certainly capable of writing one in Java. The only even vaguely recent flaw I can remember in the JRE was, as you say, in the part written in C (I think in some image loading code). It takes a very perverse kind of logic to say: this system which is mostly not-C and a tiny bit C keeps having security flaws in the C part, therefore we should switch to systems which are written more in C. If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit.
    - dietrichepp 12y ago
      > If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit. I'm going to quote the article again... > You're more dependent on the decisions made by the language implementers than you think. When you use Java, you don't have the opportunity to second-guess the choices that produced the JRE. And I think you're not quite getting what I'm saying: I'm not saying that "we should switch to systems which are written more in C", I'm saying that writing systems in C protects you from mistakes in the JRE (which you have no control over) in exchange for exposing you to your own mistakes (which you can control). You can then spend a large amount of time and money developing and verifying your system. The goals and constraints of your project will determine whether this is a good trade-off. I'm certain that Java is preferable for writing the vast majority of web apps, but the web is not everything. > If the tooling for verifying C is really so good, why not verify the C parts of the JRE? First, I'm going to guess that an enormous amount of static and dynamic analysis has been done on the JRE. Bugs in it are rather rare these days, given its size and complexity. However, verification tools are generally not suited to this particular task. Verification tools are better at verifying typical application code, and the JRE needs to do a lot of very unusual operations in order to work. In cases where you'd use verification, you'd also typically use a "safe" subset of C. Some of these subsets don't even permit dynamic memory allocation, or if so, only permit it at program startup. So, it may actually be more straightforward to deliver a working Mars rover in C than it would be to deliver a verified JRE. Neither task is easy.

lmm 12y ago

At the point where you're using a theorem prover you're not really writing C any more (I mean, do you count ATS as writing C?). It's a perfectly good way to produce reliable code, sure. But I'm pretty sure it's not what the article is advocating. > And then, as ill as you speak of C, you turn around and plug your Java systems into C systems, such as Varnish, Nginx, Apache, PostgreSQL, or thousands others that you use every day, not to mention the OS itself. I do my best to minimize the C surface, and I worry about what I am exposing. E.g. I don't put Apache/Nginx/etc. anywhere in my stack (I either route directly to the JVM or use an Erlang load balancer), which means I wasn't running around patching them in the wake of Heartbleed. I'd use e.g. Riak over PostgreSQL wherever possible.

spc476 12y ago
Erlang is written in C, and the latest version is 456,000 lines of C. You might want to double think your reliance on such unstable technology.
dietrichepp 12y ago
I'm just taking two lines from the article: "Reliability and proven tools are even more important than libraries"... in this case, there are a lot of proven tools for writing C programs, including the theorem provers. And "You're more dependent on the decisions made by the language implementers than you think"... there have been a lot of flaws in the JRE over time, most of them from the parts of the JRE that are written in C. If you had been writing in C, you could have avoided those flaws if you were in the top 2% most diligent and careful C programmers, because the C tools are rock solid, whereas Java tools haven't been (January 2013 is still pretty recent). Problems in libraries, such as heartbleed, can be mitigated in C using the same tools that you'd use in Java. Process isolation is great. Of course, if you are writing your web app in C then I am going to replace you with someone else. But the web is not everything.
- heinrich5991 12y ago
  What is such a theorem prover? I'm interested in it for trying to prove properties of my own programs...
- lmm 12y ago
  The January 2013 flaws affected end users running the browser plugin, not systems written in Java. I suppose if you had a system that allowed users to submit their own bytecode and used Java's native facilities for handling this, then you'd be vulnerable. But nothing forces you to do that; someone who's capable of writing a safe bytecode verifier in C is certainly capable of writing one in Java. The only even vaguely recent flaw I can remember in the JRE was, as you say, in the part written in C (I think in some image loading code). It takes a very perverse kind of logic to say: this system which is mostly not-C and a tiny bit C keeps having security flaws in the C part, therefore we should switch to systems which are written more in C. If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit.
  - dietrichepp 12y ago
    > If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit. I'm going to quote the article again... > You're more dependent on the decisions made by the language implementers than you think. When you use Java, you don't have the opportunity to second-guess the choices that produced the JRE. And I think you're not quite getting what I'm saying: I'm not saying that "we should switch to systems which are written more in C", I'm saying that writing systems in C protects you from mistakes in the JRE (which you have no control over) in exchange for exposing you to your own mistakes (which you can control). You can then spend a large amount of time and money developing and verifying your system. The goals and constraints of your project will determine whether this is a good trade-off. I'm certain that Java is preferable for writing the vast majority of web apps, but the web is not everything. > If the tooling for verifying C is really so good, why not verify the C parts of the JRE? First, I'm going to guess that an enormous amount of static and dynamic analysis has been done on the JRE. Bugs in it are rather rare these days, given its size and complexity. However, verification tools are generally not suited to this particular task. Verification tools are better at verifying typical application code, and the JRE needs to do a lot of very unusual operations in order to work. In cases where you'd use verification, you'd also typically use a "safe" subset of C. Some of these subsets don't even permit dynamic memory allocation, or if so, only permit it at program startup. So, it may actually be more straightforward to deliver a working Mars rover in C than it would be to deliver a verified JRE. Neither task is easy.