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

61–70 of 155 posts

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

#61

Post by robmccoll »

optforfon wrote: post #55

- What tools do they use for error checking/linting? - Well... why C？ If ｃｏｒｒｅｃｔｎｅｓｓ ｉｓ ｓｏ ｉｍｐｏｒｔａｎｔ．．． ｓｕｒｅｌｙ ｔｈｅｒｅ ａｒｅ ｂｅｔｔｅｒ ｌａｎｇｕａｇｅｓ ｔｈａｎ Ｃ － not only better type systems, but also theorem proving and other fancy modern features. It doesn't even have to be garbage collected. － ａｔ ｔｈｅ ｖｅｒｙ ｌｅａｓｔ ａｒｅ ｔｈｅｙ ｕｓｉｎｇ ｌａｎｇｕａｇｅ ｅｘｔｅｎｓｉｏｎｓ？ ｅｖｅｎ ｇｃｃ ｐｒｉｍｉｔｖｅｓ ｗｏｕｌｄ ｈｅｌｐ！

I don't know for sure, but if I had to guess, it's that they are on relatively new, uncommon, or limited architectures for which a variety of compilers just don't exist. Many other compilers depend on being bootstrapped through C and many other runtimes depend on some subset of standard C library functions. Also if you stick to a certain part of C and write very simple code, it can be safe and more importantly very predictable. In embedded usage, you need to know that the execution time can fall within a bound. It can also be important to shy away from getting too high level in architecture or concept because that can hide complex but catastrophic logical bugs.

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

#62

Post by adrianratnapala »

elcapitan wrote: post #46
corecoder wrote: post #21

Earlier quoted context omitted.

They mean that it's hard to write a static analysis tool that can determine if functions using recursion will ever terminate or not.

Just out of curiosity, why is that harder than writing a static analysis that determines if a loop with condition will finish?

Rule #2 is "Fixed Upper Bound for Loops".

Although they define this flexibily as "It should be possible for a verification tool to prove statically that a preset upper-bound on the number of iteration of a loop can’t be exceeded."

So any loops where they can in fact write a verifier is simple enough.

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

#63

Post by lmm »

msoucy wrote: post #18
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 ) ?

Haskell's type system protects from a certain class of bug, but it can't prevent logic errors - something like using won't trigger a build error, but it certainly is a bug.

Sometimes you can express the relevant relationship in the type system. Just adding types to an existing program won't tell you much, but if you work with the type system it's possible to move a lot of your business logic there.

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

#64

Post by TickleSteve »

Unklejoe wrote: post #41
petra wrote: post #13

Earlier quoted context omitted.

How do you analyze worst case ? don't you need to know what calls what, up to what depth, and that's dynamic by nature ?

As said by TickleSteve, you define the worst case rather than analyze it. As for the stack usage requirements, it seems like this could be determined statically by some parametric process, but I’m no expert on this. Does anyone see a reason why there couldn’t be some algorithm to statically analyze some code to derive the worst case stack usage? For example, take every function and assume that every variable declarat…

...in a typical GCC based system, you can for example use "-fstack-usage" and "-fcallgraph-info" to determine a worst case.

(tho that takes a bit of analysis, there are tools around that can automate this).

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

#65

Post by [deleted] »

delinka wrote: post #58
optforfon wrote: post #55

- What tools do they use for error checking/linting? - Well... why C？ If ｃｏｒｒｅｃｔｎｅｓｓ ｉｓ ｓｏ ｉｍｐｏｒｔａｎｔ．．． ｓｕｒｅｌｙ ｔｈｅｒｅ ａｒｅ ｂｅｔｔｅｒ ｌａｎｇｕａｇｅｓ ｔｈａｎ Ｃ － not only better type systems, but also theorem proving and other fancy modern features. It doesn't even have to be garbage collected. － ａｔ ｔｈｅ ｖｅｒｙ ｌｅａｓｔ ａｒｅ ｔｈｅｙ ｕｓｉｎｇ ｌａｎｇｕａｇｅ ｅｘｔｅｎｓｉｏｎｓ？ ｅｖｅｎ ｇｃｃ ｐｒｉｍｉｔｖｅｓ ｗｏｕｌｄ ｈｅｌｐ！

This formatting doesn't match the rest of HN which makes it difficult to read. Is this a bug somewhere?

[deleted]

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

#66

Post by vonmoltke »

Bromskloss wrote: post #56
TickleSteve wrote: post #12

Earlier quoted context omitted.

task == thread of control. (Seriously? downvoted because I gave a direct, true answer to a question?)

I'm afraid I don't know what you mean by that either.

It must unknowingly be embedded-specific terminology, because I knew exactly what he was talking about.

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

#67

Post by drauh »

delinka wrote: post #58
optforfon wrote: post #55

- What tools do they use for error checking/linting? - Well... why C？ If ｃｏｒｒｅｃｔｎｅｓｓ ｉｓ ｓｏ ｉｍｐｏｒｔａｎｔ．．． ｓｕｒｅｌｙ ｔｈｅｒｅ ａｒｅ ｂｅｔｔｅｒ ｌａｎｇｕａｇｅｓ ｔｈａｎ Ｃ － not only better type systems, but also theorem proving and other fancy modern features. It doesn't even have to be garbage collected. － ａｔ ｔｈｅ ｖｅｒｙ ｌｅａｓｔ ａｒｅ ｔｈｅｙ ｕｓｉｎｇ ｌａｎｇｕａｇｅ ｅｘｔｅｎｓｉｏｎｓ？ ｅｖｅｎ ｇｃｃ ｐｒｉｍｉｔｖｅｓ ｗｏｕｌｄ ｈｅｌｐ！

This formatting doesn't match the rest of HN which makes it difficult to read. Is this a bug somewhere?

They seem to be different Unicode codepoints: FULLWIDTH LATIN SMALL LETTER

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

#68

Post by vonmoltke »

corecoder wrote: post #21
elcapitan wrote: post #7

> Do not use [..] direct or indirect recursion. Ok.. I get it that they don't want their C programmers to do that, but do they also mean that this is to "complex" for normal developers to implement in a fault-free manner?

They mean that it's hard to write a static analysis tool that can determine if functions using recursion will ever terminate or not.

It also puts a lot of stress on the stack of machines that may not have much stack to go around.

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

#69

Post by oconnore »

kowdermeister wrote: post #39
sa1 wrote: post #31

Earlier quoted context omitted.

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.

You can't prove intent.

However, you can consider the formal specification of your intent (the type), to be an example of fully declarative programming.

Since you write your type without any care about how it might be executed -- the holy grail of abstraction -- you are less likely to make errors.

When using a type system that isn't capable of fully specifying what you're doing (i.e. Haskell), you are of course subject to making implementation errors within the range of possible programs that type check. But in practice it's usually enough to catch the sorts of mistakes that you're likely to make.

Post reply on HN