Software crisis: the next generation (2016) • Hacker News Board

Re: Software crisis: the next generation (2016)

#61

Post by naasking » Thu, Jan 11, 2018, 5:07 PM UTC

Annatar wrote: post #54

naasking wrote: post #52

Earlier quoted context omitted.

> For 20 years I’ve been writing entire applications in AWK, a dynamically typed language, and not once were any of the bugs due to typing. If you spent 20 years writing serious programs in Awk, I'm not convinced you know what real static typing is.

I had Ada as part of the core curriculum, just so we're clear. And being part of the cracking / demo scene, I grew up writing in MOS 6502 and MC68000 moving on to UltraSPARC assembler, so I just might know a thing or two about typing and what it actually translates to at the machine level. But, hey, barring suddenly landing a job working on SmartOS / illumos, that's also why I want to exit the computer industry: some…

Machine level translation of language abstractions isn't relevant. Ada is an ok typed language, but still limited in many ways, but that's neither here nor there.

The reason I can confidently state that you don't know what typing is, is because a type system is simply a means to prove propositions about your program. A type is a proposition. Any proposition, really. Most type systems employ propositions about simple equalities, inequalities and subsets, but there exist type systems that prove the absence of data races, deadlocks, the conformance to protocols, and even the time and space complexity of programs.

So when you claim that none of your program bugs were a result of poor typing, you're literally claiming that none of these bugs resulted from treating a false proposition as if it were true. That's just nonsense. Literally every bug results from treating a false proposition as true.

Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not. Which is by itself exceedingly unbelievable.

And even if you are that perfect, you clearly don't have a perfect understanding of your fellow, imperfect human beings who need tools to actually help them avoid mistakes.

Re: Software crisis: the next generation (2016)

#62

Post by flavio81 » Thu, Jan 11, 2018, 7:49 PM UTC

golergka wrote: post #56

flavio81 wrote: post #51

Earlier quoted context omitted.

>If most of your experience was with statically typed systems, it's just logical you would have very little experience with bugs that are prevented by statically typed systems And then, when I used a dynamically typed language (Python) for serious stuff for the first time, I didn't miss those checks. Sincerely, the great majority of those "bugs that are prevented by statically typed systems" are bugs that only a novi…

> It's only dynamically typed languages with WEAK typing the ones that give "dynamically typed" a bad name. (In)famous examples: Javascript and PHP. Perhaps your experience of dynamically typed languages has been with Javascript? Javascript, exactly. I have to admit, Python have already been mentioned here a couple of times, so it seems that I have to try using it in some big project to get more experience on the mat…

Thanks for replying, because I didn't mean to be rude to you.

>Javascript, exactly.

Well, then consider you had experience with only one dynamically typed language, and one with a notoriously poor type system. Thus, you wrote: "But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors"."

If we consider "dynamically typed languages" == "Javascript", then your assertion is correct: Javascript isn't particularly fast (although it's decent in speed), and no, it doesn't help you prevent errors. But this is not because of it being "dynamically typed". It is because of many other things: Weakly typed, lack of good exception handling mechanism, lack of a good module/encapsulation system, and so on.

>Python have already been mentioned here a couple of times, so it seems that I have to try using it in some big project to get more experience on the matter.

Python is easy to learn and one of my favorites (i've used it extensively), but, however, it wouldn't be my candidate for "really good dynamically typed language". Python isn't too fast, it has some limitations for concurrency, it also has some awkward limitations for functional programming, it's OOP system isn't particularly great (but still, useful) and so on. But for example python brings something that neither Java nor C nor Javascript have and do help a lot in preventing errors: Named arguments (named function parameters.)

I like Python because it's fun/comfortable to use.

But If you want to explore really good dynamically typed languages, you should try taking a look at Common Lisp and Julia. Both of them have:

* Very strong typing

* A flexible type system

* Lots of data types (i.e. complex numbers, fractions, arbitrary length numbers)

* A very, very powerful OOP system (particularly Common Lisp... far more powerful than what you'd get on Java, C++, Objective-C or even Smalltalk)

* A decent package/module system

* Speed that can be tailored to get close to C

* Easy parallel and distributed computing (particularly Julia)

* Metaprogramming (particularly Common Lisp)

* Easy interop with C

Julia is modern and was inspired by Common Lisp. Common Lisp started in the mid '80s and it's still one of the most advanced languages you can find today. I'd say Julia is probably easier to learn and focused on scientific computing, and that CL is probably a bit more powerful and more general purpose.

Common Lisp also has an exception handling mechanism called "conditions and restarts" that is simply exemplary, because it's not only intended for catching exceptions but also for overcoming them.

You would be surprised by the safety provided by Common Lisp -- the runtime will complain if anything looks suspicious or if some error is caught; will then give you a very explicit explanation of what's wrong, and then it will give you alternatives of action. You could even go to the source code, correct the function that has the mistake, recompile that specific function, while the code is running, and watch your program continuing running, this time correctly.

Not many languages can do that.

Re: Software crisis: the next generation (2016)

#63

Post by Annatar » Fri, Jan 12, 2018, 9:38 AM UTC

naasking wrote: post #61

Annatar wrote: post #54

Earlier quoted context omitted.

I had Ada as part of the core curriculum, just so we're clear. And being part of the cracking / demo scene, I grew up writing in MOS 6502 and MC68000 moving on to UltraSPARC assembler, so I just might know a thing or two about typing and what it actually translates to at the machine level. But, hey, barring suddenly landing a job working on SmartOS / illumos, that's also why I want to exit the computer industry: some…

Machine level translation of language abstractions isn't relevant. Ada is an ok typed language, but still limited in many ways, but that's neither here nor there. The reason I can confidently state that you don't know what typing is, is because a type system is simply a means to prove propositions about your program. A type is a proposition. Any proposition, really. Most type systems employ propositions about simple…

"Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not."

How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. It can't be any other way (unless your central processing unit is designed by intel corporation)!

In the line of work I do I don't normally design systems with locking, but I have designed them in the past and they worked fine by the way of empirical testing (purposely trying to cause a deadlock). I didn't need a formal system to prove it, nor would I ever trust such a system to ensure that my code or logic were correct.

The rest is pure philosophy about provable code, and I've little appreciation for that: even Donald Knuth famously wrote

beware of bugs in the above code; I have only proved it correct, not tried it.

That's very instructive for one seeking insight, and I urge you to rethink your position on strong typing, because it's not the panacea you appear to believe it is. It doesn't make a difference if one is not a good programmer: in that case, nothing will save one. Not even being able to formally prove one's program logic is correct.

Finally, I leave you with a theme from my childhood when I was learning to program:

natural born coders

I recommend meditating on it if you intend to continue working in the computer industry, because it's a real thing. They are few, but they do exist, and their work is unbelievable to behold. Even without them having used a strongly typed system to formally prove their code correct.

https://www.youtube.com/watch?v=hvX6Y2bW4Z0

Re: Software crisis: the next generation (2016)

#64

Post by golergka » Fri, Jan 12, 2018, 10:21 AM UTC

flavio81 wrote: post #62

golergka wrote: post #56

Earlier quoted context omitted.

> It's only dynamically typed languages with WEAK typing the ones that give "dynamically typed" a bad name. (In)famous examples: Javascript and PHP. Perhaps your experience of dynamically typed languages has been with Javascript? Javascript, exactly. I have to admit, Python have already been mentioned here a couple of times, so it seems that I have to try using it in some big project to get more experience on the mat…

Thanks for replying, because I didn't mean to be rude to you. >Javascript, exactly. Well, then consider you had experience with only one dynamically typed language, and one with a notoriously poor type system. Thus, you wrote: "But some people are still praising dynamically typed languages for their "speed" and "lack of compiler errors"." If we consider "dynamically typed languages" == "Javascript", then your asserti…

Well, I've gone through SICP (book and exercises), so I might say that I have some familiarity with Lisp, as well as Python - but it's one thing to do toy or personal projects and another altogether to work on a full-scale project with several collaborators and a complicated history. There's a whole class of issues you experience in such a project that really shed a new light on a language as a tool of communication between developers.

By the way, the speed I mentioned is speed of development. Both Javascript and Python are used nowadays in speed-critical applications, with NodeJS on the servers and Python in various roles in big data and machine learning because the critical path is actually done on C level (I/O for NodeJS and GPU/math stuff for Python) while these languages are in charge of the stuff that is not that critical in terms of speed but much more complicated in terms of logic. This brings me to think that if you use a language on an appropriate domain and separate concerns between domains in a good way, it wouldn't matter if the language itself isn't that fast.

Re: Software crisis: the next generation (2016)

#65

Post by naasking » Fri, Jan 12, 2018, 2:55 PM UTC

Annatar wrote: post #63

naasking wrote: post #61

Earlier quoted context omitted.

Machine level translation of language abstractions isn't relevant. Ada is an ok typed language, but still limited in many ways, but that's neither here nor there. The reason I can confidently state that you don't know what typing is, is because a type system is simply a means to prove propositions about your program. A type is a proposition. Any proposition, really. Most type systems employ propositions about simple…

"Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not." How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. It can't be any other way (unless yo…

> How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't.

Testing equality with a constant is not the only equality test you make in programs. Firstly, what assurances do you even have that d0 actually is a byte? d0 could be a pointer so a byte comparison is invalid, unless you're doing some low-order bit pointer tagging.

Secondly, comparisons where both operands are variables are where it starts getting murkier.

> In the line of work I do I don't normally design systems with locking, but I have designed them in the past and they worked fine by the way of empirical testing (purposely trying to cause a deadlock). I didn't need a formal system to prove it, nor would I ever trust such a system to ensure that my code or logic were correct.

You certainly need a formal system to prove it if you want to guarantee absence of deadlocks. You literally just said that you couldn't empirically trigger a deadlock, but that doesn't entail deadlocks don't exist.

As for your distrust, I'm not interested in non-factual religious arguments.

As for Knuth, you do realize he thinks that typical testing practices are often stupid, and that quote is him poking fun right? He informally proves most of the code he works with, and only does testing when he's still exploring an idea and he doesn't yet know what he wants.

> It doesn't make a difference if one is not a good programmer: in that case, nothing will save one. Not even being able to formally prove one's program logic is correct.

What kind absurdity is this? If you can prove your program's logic is correct, your program's logic is correct even if you're a bad programmer. It's a literal tautology.

Finally, I have no idea why "natural born coders" has anything to do with what this thread is about. We're talking about what should be the standards and norms across a whole industry, not a select few who might not need them. Typing is not a panacea, but results are undeniably better with a decent, modern type system than without.

Re: Software crisis: the next generation (2016)

#66

Post by Annatar » Sat, Jan 13, 2018, 8:25 AM UTC

naasking wrote: post #65

Annatar wrote: post #63

Earlier quoted context omitted.

"Even if we just stick with type systems dealing with simple equalities, like ML, claiming that none of your bugs would have been caught by types means that you never mistakenly considered two values as equal when they were not." How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. It can't be any other way (unless yo…

> How could I mistake two values as equal when they were not? If I'm doing a cmp.b d0, #$31, either d0 will contain #$31 and it will be a byte or it won't. Testing equality with a constant is not the only equality test you make in programs. Firstly, what assurances do you even have that d0 actually is a byte? d0 could be a pointer so a byte comparison is invalid, unless you're doing some low-order bit pointer tagging…

“Firstly, what assurances do you even have that d0 actually is a byte?“

Because of .b in cmp.b; in assembler you control exactly what goes in and what goes out. If you are comparing bytes, then bytes it must be; the rest of the register is ignored. And if you’re cmp.l d0, #$31 comparing longwords, then you already know what you’re expecting and the very nature of the way that works is that it either works or doesn’t. cmp.b d0,d1, same deal.

You’re trying to elevate something trivial (formal proof) to something more valuable and important than it really is.

And one more thing: a bad programmer will never make an effort to formally prove the logic in his program or use a strongly typed system for that matter. And a good programmer? Well, considering that Rust is utter overcomplicated garbage mishmash, that pretty much only leaves Ada as the only realistic tool of choice, but Ada is also not a very good tool: one thing that remains seared in my mind was the acute lack of documentation on the language, especially on how to solve real world problems, which makes Ada impractical. Where does that leave us? It leaves us with our own brain, knowledge, experience and insight to not write crappy software. Sorry that you feel that strong typing is a valuable tool, but practice and reality disagree with you, as is often the case in life. Better concentrate on how to write high quality software without it, or else you won’t get too far, and what benefits you do claim aren’t worth it, no matter how well it sounds in theory.

Is being able to formally prove one’s program logic better than not being able to do so? Of course. But the programming languages, the tools to do that, are utter overcomplicated garbage. You’d have an easier time and be more productive coding in assembler where you control everything, then using a piece of overcomplicated trash fire that is Rust, for example.

The entire typing thing is really just a made up crutch necessitated by artificial abstractions by high level programming languages: when I look at the data you’re sending me from the high level language in my assembler code, it’s all bits, the only thing the hardware understands, the reality. So do yourself a favor, don’t make it more complex than it needs to be. Computers are already an overcomplicated pain in the ass, let’s not try to turn it into rocket science, because it can never be that.