Live data from Hacker News

Software crisis: the next generation (2016)

habitatchronicles.com

11–20 of 66 posts

Re: Software crisis: the next generation (2016)

#11
post #9
post #4

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors".

Good to see the strict typing of C has saved it from most security issues. i think it it is quite facetious to put it down to type systems.

C does not have particularly strict typing

Re: Software crisis: the next generation (2016)

#12
post #9
post #4

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors".

Good to see the strict typing of C has saved it from most security issues. i think it it is quite facetious to put it down to type systems.

There are different type systems (think C vs Rust), and having one is always better than having none. C still prevents some issues you can have with assembly.

Re: Software crisis: the next generation (2016)

#13
post #4

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors".

When you talk about static typing as providing some form of formal verification, you really can only talk about languages with advanced type systems like Haskell. Type systems like those in Java and C# give you very little formal verification (and I say this as someone who programs daily in C# for work and Python and Common Lisp for fun). What Java-like type systems give you is confidence in refactoring, which is not…

I work with C# full-time and it's type system constantly helps me. Of course, it's not Haskell or Rust, but it is still so much better than my Javascript experience. Anonymous types, generic containers and interfaces are usually enough for my needs.

Can you please go into some detail about heterogenous tuples in Python? I've never used it to build big long-lasting systems so I be not aware of some of it's type capabilities.

Re: Software crisis: the next generation (2016)

#14
post #6

“The reason this stuff is crap is far more basic. It’s because better-than-crap costs a lot more, and crap is usually sufficient. ... ... ... Every dollar put into making software less crappy can’t be spent on other things we might also want, the list of which is basically endless.“ Software is crap because humans on the whole have an extremely difficult time reasoning through all the possible logic flows. Software i…

Do all other Industries manage it though? If they did we wouldn't have product recalls or any need for "consumer safety watchdogs". The problem is arguably worse in software but software can also be (relatively) easily patched later so a somewhat more lax attitude to quality on systems that are not safety critical makes some degree of sense.

Re: Software crisis: the next generation (2016)

#15
post #6

“The reason this stuff is crap is far more basic. It’s because better-than-crap costs a lot more, and crap is usually sufficient. ... ... ... Every dollar put into making software less crappy can’t be spent on other things we might also want, the list of which is basically endless.“ Software is crap because humans on the whole have an extremely difficult time reasoning through all the possible logic flows. Software i…

> Software is crap because humans on the whole have an extremely difficult time reasoning through all the possible logic flows.

But we have tools and techniques that make this easier. Why don't we use them?

Also, I don't think 100% correctness is the ultimate goal of this article. Software is probably nowhere even near that correctness level firstly, and secondly, software is also partly crap because it doesn't run any faster than it did 30 years ago despite tremendous performance advances in our hardware.

> What does that make us? It makes us jerk-offs, that’s what it makes us.

Let's be honest, software as it currently is written is considerably more complex than most other engineered systems that we take for granted.

That said, we've had tools and techniques to mitigate a lot of this complexity, and to have computers double-check our work (eg. type systems and model checking), but we don't really use them as much as we should. What's worse, we even use tools that are intentionally intractable to any kind of work checking/validation (like dynamically typed languages).

There's really no excuse for this.

Re: Software crisis: the next generation (2016)

#16
post #9
post #4

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors".

Good to see the strict typing of C has saved it from most security issues. i think it it is quite facetious to put it down to type systems.

An unsound type system doesn't prove anything about type systems. Doubly so if you don't actually use types and you're just exploiting that unsoundness with pervasive casting.

Re: Software crisis: the next generation (2016)

#17
post #5

> Anybody who’s seen the systems inside a major tech company knows this is true. Or a minor tech company. Or the insides of any product with a software component. Anybody who's seen the sun rising east and setting west knows that this is true: the Sun rotates around the Earth. The other, less-obvious alternative, is that software is NOT crap, we just like to complain a lot. And it's just so easy & fun to blame everyt…

If our metric for "good" is based solely on what people choose to use, then one is forced to admit that we also have generally good security and privacy safeguards.

Actually, I kinda agree with that assessment. "Good enough" is never good enough for academics, but practical reality is different.

Re: Software crisis: the next generation (2016)

#18
post #4

We have some formal verification, it's called typed systems. Very limited, I know. But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors".

When you talk about static typing as providing some form of formal verification, you really can only talk about languages with advanced type systems like Haskell. Type systems like those in Java and C# give you very little formal verification (and I say this as someone who programs daily in C# for work and Python and Common Lisp for fun). What Java-like type systems give you is confidence in refactoring, which is not…

> Type systems like those in Java and C# give you very little formal verification [...] What Java-like type systems give you is confidence in refactoring, which is not nothing, but it is not formal verification.

You might be surprised to hear that you can prove a large class of programs correct using plain ol' Java types [1].

[1] http://lambda-the-ultimate.org/node/5387

Re: Software crisis: the next generation (2016)

#19
post #6

“The reason this stuff is crap is far more basic. It’s because better-than-crap costs a lot more, and crap is usually sufficient. ... ... ... Every dollar put into making software less crappy can’t be spent on other things we might also want, the list of which is basically endless.“ Software is crap because humans on the whole have an extremely difficult time reasoning through all the possible logic flows. Software i…

> All other industries manage to deliver complete, working products;

Ha. If you were more heavily involved in those industries, I believe you would find that they all have similar problems because the article is right: we make tradeoffs all the time, in everything, so very little is ever as good as it could be. You just don't notice it because you don't have a lot of knowledge about it, their products are "good enough" for you and you don't think about it beyond that. Sound familiar?

Re: Software crisis: the next generation (2016)

#20
post #6

“The reason this stuff is crap is far more basic. It’s because better-than-crap costs a lot more, and crap is usually sufficient. ... ... ... Every dollar put into making software less crappy can’t be spent on other things we might also want, the list of which is basically endless.“ Software is crap because humans on the whole have an extremely difficult time reasoning through all the possible logic flows. Software i…

> All other industries manage to deliver complete, working products; we are the only industry which doesn’t; computers and software never work 100% correctly.

Have you ever worked in other industries? This... is not true. We're not snow flakes.

Post reply on HN