Is Uncle Bob serious?

Post by tpush » Tue, Oct 10, 2017, 1:47 PM UTC

tome wrote: post #75

tpush wrote: post #26

Curiously, in the list of possible future tools for more reliability type systems are absent. Looking at the authors bio: "I love solving tough problems with Python and PHP". Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). If you want a property to uphold, formulate it as a type. The compiler verifies. If formulating the type is to laborious,…

> Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). If you want a property to uphold, formulate it as a type. The compiler verifies. I'm a massive Haskell proponent and I'm calling you out because you're doing typed programming a massive injustice with this kind of overinflated claim. There is no known type system that can get anywhere near sol…

Post by kazinator » Tue, Oct 10, 2017, 1:48 PM UTC

blub wrote: post #60

erokar wrote: post #37

Earlier quoted context omitted.

> Type systems to me seem to be (I'm not exaggerating) the answer to all software reliability problems (barring social ones). That's the thing though, the "social problems" are the important problems. I think it's a given you should use strong type systems in safety critical software — Haskell, for instance. But look at the quote from Dr Nancy Leveson: I've been doing this for thirty-six years. I've read hundreds of…

I'm curious how OP would prevent the Therac incident through type systems... Key quote: "Previous models had hardware interlocks in place to prevent this, but Therac-25 had removed them, depending instead on software interlocks for safety." Or even better how type systems could work around data integrity errors in RAM without ECC.

Post by sheepmullet » Tue, Oct 10, 2017, 1:55 PM UTC

gipp wrote: post #68

blub wrote: post #50

Earlier quoted context omitted.

Type systems are not enough. I'm not sure they're even a good starting point for safety critical software, but they might be good for e.g browsers. You're thinking at code level, people like Leveson, Knight and others are thinking at system level. The end goal is to have a safe system, not e.g avoid null pointer exceptions through optional types.

I'm not sure you're familiar enough with what a sufficiently powerful type system can accomplish. A full dependent type system is sufficient to statically prove that code meets a given specification. We're not just talking about ints and strings and optionals when we talk about type systems for correct software. See Curry-Howard correspondence.

Post by 12312312qqq » Tue, Oct 10, 2017, 2:01 PM UTC

tptacek wrote: post #34

tpush wrote: post #30

Earlier quoted context omitted.

Because he is not random but influential, simple as that.

Why is he influential? Because he wrote some books? That's the reason given downthread. Past a fairly low karma threshold, so could any commenter on HN.

Post by kazinator » Tue, Oct 10, 2017, 2:04 PM UTC

gipp wrote: post #68

blub wrote: post #50

Earlier quoted context omitted.

Type systems are not enough. I'm not sure they're even a good starting point for safety critical software, but they might be good for e.g browsers. You're thinking at code level, people like Leveson, Knight and others are thinking at system level. The end goal is to have a safe system, not e.g avoid null pointer exceptions through optional types.

I'm not sure you're familiar enough with what a sufficiently powerful type system can accomplish. A full dependent type system is sufficient to statically prove that code meets a given specification. We're not just talking about ints and strings and optionals when we talk about type systems for correct software. See Curry-Howard correspondence.