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.
Software crisis: the next generation (2016)
11–20 of 66 posts
Re: Software crisis: the next generation (2016)
#12We 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.
Re: Software crisis: the next generation (2016)
#13We 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…
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“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…
Re: Software crisis: the next generation (2016)
#15“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…
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)
#16We 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.
Re: Software crisis: the next generation (2016)
#17> 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…
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)
#18We 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…
You might be surprised to hear that you can prove a large class of programs correct using plain ol' Java types [1].
Re: Software crisis: the next generation (2016)
#19“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…
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“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…
Have you ever worked in other industries? This... is not true. We're not snow flakes.