Live data from Hacker News

The Power of Ten – Rules for Developing Safety Critical Code

spinroot.com

31–40 of 155 posts

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

#31
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 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).

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

#32
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 ) ?

If you can do the wrong thing perfectly, then you have a bug.

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

#33
post #25
post #14

Speaking from experience, the biggest problem with NASA's software engineering requirements ( http://nodis3.gsfc.nasa.gov/displayDir.cfm?t=NPR&c=7150&s=2B ) is the way that they tend to feed down into non-safety critical projects. It's getting better though.

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.

Good points, but mainly I was referring to the need to maintain extensive documentation purely for the satisfaction of bureaucratic review (though that point was in my head).

Example: All projects that are to be released must demonstrate that they are maintaining one of these:

http://nodis3.gsfc.nasa.gov/displayDir.cfm?Internal_ID=N_PR_...

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

#34
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 ) ?

It's not particularly true.

What they're saying is that Haskel (and Scala, and others) have such good type systems your data should never be wrong.

That has nothing to do with logic, and so if your code should be `if (foo)` and you write `if (bar)` or `if (!foo)` there is no way for a type system to catch that.

Additionally, there are a lot of constraints you can't capture with type systems. For example: given type Foo, type Bar extending Foo, and types * extending Foo, my type should extend Foo but not be or extend Bar.

Even just with raw data, imagine if your function required and was only valid if you passed in a prime number, or an even integer between 2 and 22, or a "sentence contained of 3 or more words none of which are Chinese" etc. It gets hard very quickly.

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

#35
This is an all-time classic.

Too bad that the article doesn't mention the original paper:

http://pixelscommander.com/wp-content/uploads/2014/12/P10.pd...

Some interesting HN discussions around applying these NASA coding standards to JavaScript:

https://news.ycombinator.com/item?id=8856226

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

#36
I posted a write-up of Dr. Holzmann's talk "Mars Code" which he gave at USENIX Hot Topics in System Dependability '12 (http://www.verticalsysadmin.com/making_robust_software/), about how NASA/JPL writes and tests software that survives the rigors of interplanetary travel; planetary entry, descent, and landing; and operation in another world. :)

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

#37
post #25
post #14

Speaking from experience, the biggest problem with NASA's software engineering requirements ( http://nodis3.gsfc.nasa.gov/displayDir.cfm?t=NPR&c=7150&s=2B ) is the way that they tend to feed down into non-safety critical projects. It's getting better though.

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.

Type based programming does not quite work in weakly typed languages.

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

#38
post #37
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.

Type based programming does not quite work in weakly typed languages.

I think you should take what he said as saying we should get rid of those

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

#39
post #31

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).

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.

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

#40
post #3

Found the rule `There shall be no use of dynamic memory allocation after task initialization.` They must use pre-allocated string buffers for some of the task's. Though I figured if you're doing a flight controller for a jet fighter or sate-light you don't need a lot of string parsing.

dynamic memory allocation is very much frowned upon in embedded systems, not just for strings. Everything should be static and deterministic at all times. This is the easiest/only way to ensure you have no resource issues. You should always (statically) allocate for maximum/worst case.. because you have analysed your worst-case, haven't you?

That rhetorical question touches on a very important point, and I agree 100%. Dynamic memory allocation allows programmers to absolve themselves of considering worst case (memory usage) scenarios. As long as they handle allocation failures, their program should function predictably under all memory circumstances (in reality, we know this isn’t always the case, especially when the failure occurs deep in the call stack). The problem is predicting the memory circumstance itself. The way your program behaves is essentially tied to something external, which makes it that much harder to predict the overall behavior. This scheme makes sense in environments where you really have no idea how much memory will be available to you, such as a conventional PC program, but not on a system that has a single dedicated purpose. One could make the argument that if the program gracefully handles an allocation failure, then there should be no problem. My counter argument would be that in many embedded systems, it’s better to have a predictable, but low failure threshold as opposed to a potentially higher, but unpredictable failure threshold.

Another analogy: I would rather have a program with a 100% chance of hitting a bug under a well understood circumstance rather than a program with a 0.00001% chance of hitting a bug under an unpredictable/unknown circumstance.

In an embedded environment, you have complete control over the system and all aspects of it (or at least you should).

You often need to understand the behavior of your system under all circumstances, and that becomes _much_ easier to do when you operate with fixed size data structures because you now know exactly when you will run out of memory.

Consider a hypothetical embedded system where you’re creating a sub-module which must handle external events by means of a message queue. If you know that you can only have three possible events, you can statically allocate your message queue to be 3 deep to ensure that you will never drop an event. If you were to use dynamic memory allocation, you can’t make that guarantee because you don’t know what the other components of the system are doing (and how much memory they’re allocating). Even if there are no other allocations taking place, you still can’t guarantee that yours will succeed due to the possibility of fragmentation.

Statically allocating your buffers ensures that if the program can be loaded in the first place, you can predict with 100% certainty your program will be able to handle those 3 events.

Post reply on HN