Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Power of Ten – Rules for Developing Safety Critical Code

spinroot.com

Post reply on HN
Print view View original

111–120 of 155 posts

Re: The Power of Ten – Rules for Developing Safety Critical Code

#111

Post by sfifs »

smaddox wrote: post #96
kowdermeister wrote: post #39

Earlier quoted context omitted.

If I grasp that right, it says that if something is provable mathematically, then you can write a program for it with an equal meaning. I still don't see how that prevents user error. My question is then how do you mathematically prove intent? Also, how far should "sufficiently advanced" be? We already have a tool for that in the forms of unit tests and types does help if the subject is abstract enough.

You need more than an advanced type system. You need a declarative constraint solving and proof system. Instead of telling the compiler how to perform a task, you would declare the assumptions and the desired relationships and then, with the help of the proof system, determine what implementation fullfills exactly those constraints.

Or you take the more practical Monte Carlo like approach - Ie Fuzzing

Re: The Power of Ten – Rules for Developing Safety Critical Code

#112

Post by marcosdumay »

xorblurb wrote: post #79
lambdadmitry wrote: post #30

Earlier quoted context omitted.

It's not "disregarded", it's eclipsed by a need to ship often and ship a lot. There is a tendency to overstate amount of problems that come from bugs because they are painful to debug. Therefore, somewhat experienced programmers are often too defensive and suspect to paralysis by analysis (of which uber-complicated and rigid typing is a sort). Even if some advanced typing system will save a few days of debugging afte…

> paralysis by analysis (of which uber-complicated and rigid typing is a sort). How "paralysis by analysis" has anything to do with typing? And how is typing uber-complicated to begin with? This is ultra basic logic... And why exactly you you think dynamic langages are exempt of typing? How does all of that has anything to do with a competitor shipping "buggy RoR-based systems a few months earlier"? You can do all ki…

> You do not abstain to put on your seat-belt just because you thing you know how to drive, nor do you disable all safety feature of whatever equipment just because you kind of think, without even the beginning of a reasoning to backup that, that you are going to do things "faster".

Lots of people do.

Yes, they often turn out dead, or missing limbs. But it's a fact that they do, to the point that industries have to police and punish people that don't use safety gear.

Developers have a similar mindset, just way less dangerous.

Re: The Power of Ten – Rules for Developing Safety Critical Code

#113

Post by Joeri »

lambdadmitry wrote: post #30
pjmlp wrote: post #25

Earlier quoted context omitted.

Sadly quality is highly disregarded in our field. I dream of the day when not making use of contracts, static analysis and type based programming is seen as quality smell and not something that only a few are allowed to make use of.

It's not "disregarded", it's eclipsed by a need to ship often and ship a lot. There is a tendency to overstate amount of problems that come from bugs because they are painful to debug. Therefore, somewhat experienced programmers are often too defensive and suspect to paralysis by analysis (of which uber-complicated and rigid typing is a sort). Even if some advanced typing system will save a few days of debugging afte…

In my experience weakly typed languages are a trade-off, where you get something to run at all sooner but to run correctly only later. It all depends on the sort of product you're making whether that's worth it. When you're building something long-lived, there is no benefit to using a weakly typed language. Yes, initial coding takes less time, but since 70% of your cost is maintenance, it is dwarfed by the time spent debugging.

Re: The Power of Ten – Rules for Developing Safety Critical Code

#114

Post by GregBuchholz »

Symmetry wrote: post #70

Regarding Rule 4 - No Large Function - I think John Carmack had a pretty good explanation on why that's not really a good thing: http://number-none.com/blow/john_carmack_on_inlined_code.htm...

>The fly-by-wire flight software for the Saab Gripen (a lightweight

>fighter) went a step further. It disallowed both subroutine calls and

>backward branches, except for the one at the bottom of the main loop.

>Control flow went forward only. Sometimes one piece of code had to leave

>a note for a later piece telling it what to do, but this worked out well

>for testing: all data was allocated statically, and monitoring those

>variables gave a clear picture of most everything the software was doing.

>The software did only the bare essentials, and of course, they were

>serious about thorough ground testing.

>No bug has ever been found in the "released for flight" versions of that code.

I was pretty excited to learn more about that style, and then I came across...

https://www.flightglobal.com/FlightPDFArchive/1989/1989%20-%...

...but I'd still like to know more about this style of programming, and languages that facilitate programming in that manner.

Re: The Power of Ten – Rules for Developing Safety Critical Code

#115

Post by ufo »

sa1 wrote: post #31
kowdermeister wrote: post #27

Earlier quoted context omitted.

I doubt that statement can be true in any programming language. Bugs come in many shapes and a functional language can prevent a fraction of it. You can have logic errors, misunderstood requirements, wrong database queries etc, the list is pretty much infinite.

The https://en.wikipedia.org/wiki/Curry–Howard_correspondence says there is a correspondence between any logical statement and a type in a sufficiently advanced type system. So yes, there are languages aimed at eliminating logic errors, and Haskell goes pretty far(though its type system isn't quite advanced enough).

Curry Howard just says that computation and proof simplification work similarly. Correctness has more to do with how rich your type system is and with how you take advantage of it during modeling (to rule out undesired program states as ill-typed)

Re: The Power of Ten – Rules for Developing Safety Critical Code

#116

Post by AnimalMuppet »

pjmlp wrote: post #22
petra wrote: post #17

If we're talking about high reliability code, one thing claimed about Haskell, is "if it compiles, it has no bugs". How close is it to the truth ? And how close are we to having that kind of capability for real-time programming(even assuming we're willing to forsake protability, community, and maximum efficiency to some extent ) ?

I imagine you will find this paper interesting "Haskell vs. Ada vs. C++ vs. Awk vs. ... An Experiment in Software Prototyping Productivity" http://haskell.cs.yale.edu/?post_type=publication&p=366

I would imagine, though, that "prototyping" and "safety critical" are on opposite ends of the spectrum...

Re: The Power of Ten – Rules for Developing Safety Critical Code

#117

Post by AnimalMuppet »

lisper wrote: post #110

Rule 0: don't write safety-critical code in C.

Nice snark, I guess, but... did you actually read the article? One of the reasons for C is that the tooling around it gives you much more support. For safety critical code, you need that, because programmers make mistakes, no matter what the language.

So if you write safety critical code in Haskell, say, you won't have a large number of the holes that C gives you. But for safety critical systems, their rules say that you can't write code that has even the possibility of falling into those holes. That makes C much safer. That leaves you with a safer C, plus tooling, vs. Haskell (or whatever your choice is) without the tooling.

So, snark aside, what is your actual alternative that you recommend?

Re: The Power of Ten – Rules for Developing Safety Critical Code

#118

Post by acveilleux »

Symmetry wrote: post #70

Regarding Rule 4 - No Large Function - I think John Carmack had a pretty good explanation on why that's not really a good thing: http://number-none.com/blow/john_carmack_on_inlined_code.htm...

It's very hard to formulate a clear and easily enforced rule that restricts complexity. No large function is one way to do it.

Really long functions that have very low complexity (very few nested control structures, ideally none) and do not contain any loops that aren't trivial are easy to reason with. They are essentially the one case I'm familiar with where longer is not worse after a point.

Re: The Power of Ten – Rules for Developing Safety Critical Code

#119

Post by dragonwriter »

GregBuchholz wrote: post #114
Symmetry wrote: post #70

Regarding Rule 4 - No Large Function - I think John Carmack had a pretty good explanation on why that's not really a good thing: http://number-none.com/blow/john_carmack_on_inlined_code.htm...

>The fly-by-wire flight software for the Saab Gripen (a lightweight >fighter) went a step further. It disallowed both subroutine calls and >backward branches, except for the one at the bottom of the main loop. >Control flow went forward only. Sometimes one piece of code had to leave >a note for a later piece telling it what to do, but this worked out well >for testing: all data was allocated statically, and monitorin…

If I read that article right, it sounds like the software fault attributed to the crash is that the "control laws" that the software implemented were improperly chosen, not that the software did not function as intended.

Which is to say, a serious problem, but if we take "bug" to mean a difference between designed function and realized function, not a "bug", and therefore not something which should tarnish the record of the coding style to which the bug-free nature of the Grippen software is attributed. The problem seems to have been at a different level than coding.

Re: The Power of Ten – Rules for Developing Safety Critical Code

#120

Post by pjmlp »

AnimalMuppet wrote: post #116
pjmlp wrote: post #22

Earlier quoted context omitted.

I imagine you will find this paper interesting "Haskell vs. Ada vs. C++ vs. Awk vs. ... An Experiment in Software Prototyping Productivity" http://haskell.cs.yale.edu/?post_type=publication&p=366

I would imagine, though, that "prototyping" and "safety critical" are on opposite ends of the spectrum...

That paper was written in a time when languages like Haskell only got funding money from DARPA if it was for researching "prototyping".

Hence the way it was written.

Post reply on HN