It is unfortunate how much confusion there is about the differences between having computers search for proofs, and having computers check proofs. The best tools for formal reasoning about general mathematics (Coq, Isabelle/HOL, etc.) combine a small amount of proof search capability, but their primary purpose is to represent and check the mathematical proofs.
If some are you are really interested in the basic theoretical and philosophical underpinnings of machine-checked proofs, I would suggest starting with this paper.
If you are considering grad schoool in computer science, then you would do well to take as much advanced-level math as possible. That is, courses that teach you about writing proofs: abstract algebra, real analysis, number theory, formal logic, etc. You likely be expected to do proofs in several core grad-level courses like algorithms, programming languages, and automata theory, and a discrete math class in your freshman year is probably not going to give you enough experience.
And with regard to proofs, one technique that you absolutely must be familiar with is proof by induction--including induction on natural numbers, induction on lists, induction on trees and any other sorts structures that you might see in computer science.
Compared to what? C++? OK, maybe.
Compared to the broad spectrum of other languages, I would have to give a definite "no". The best praise I would give it would be to call it practical.
(Sorry, I know that was not the main point of your post, but the remark just jumped out at me.)
Nasty type errors are really rare, though. Normally, you've either done something stupid and the code doesn't run at all (and you have to test everything at least once), or the types are right.
What makes a type error "nasty"? It is not the degree to which the types are different, but the potential consequences of overlooking their difference.
In my view, the principal practical advantage of static type checking system (as implemented in current languages) is their ability to catch boundary conditions. Have you ever called a Python method and forgot that it might return None? Your program works fine for a while, but it will eventually trip because you forgot to test if the return value was None. It will probably just crash with an uncaught exception, but in the process may mangle or lose data. (Users tend not to like that.:)
In general, when boundary conditions are ignored, any degree of havoc can potentially result because your code is being interpreted in a way you never intended.
One answer is exception handling, and you can sometimes use this to salvage yourself from utter disaster, but if you are catching an exception that arose from a boundary condition you didn't think of, then your exception handling is too broad!
For typical programs written in a scripting language, the coder may actually want the program to just terminate on all unconsidered boundary cases. But when a script grows into a useful application (perhaps one that is run automatically by a cron job or a web server), it is eminently useful to have some sort of guarantee that it won't crash.
I have a separate email address for slashdot. And as soon as I submitted an article that was displayed on the front page and agreed to allow that email address to be publicly visible with the article announcement, I was suddenly flooded with spam. It looks like you missed out on a golden opportunity when you submitted your article without a link to your email.:)
Yeah, and then you can watch the cheap-ass power supply short out the first time you flip the switch, and fry your video card in the process. And trust me, you are not likely to be able to track down and get any reimbursement money for other damaged hardware out of a company that sells $35 cases. For the future, I do not plan on ever buying a generic power supply or another case that comes with a built-in power supply.
Slashdot Mirror
It is unfortunate how much confusion there is about the differences between having computers search for proofs, and having computers check proofs. The best tools for formal reasoning about general mathematics (Coq, Isabelle/HOL, etc.) combine a small amount of proof search capability, but their primary purpose is to represent and check the mathematical proofs.
If some are you are really interested in the basic theoretical and philosophical underpinnings of machine-checked proofs, I would suggest starting with this paper.
And with regard to proofs, one technique that you absolutely must be familiar with is proof by induction--including induction on natural numbers, induction on lists, induction on trees and any other sorts structures that you might see in computer science.
(Sorry, I know that was not the main point of your post, but the remark just jumped out at me.)
What makes a type error "nasty"? It is not the degree to which the types are different, but the potential consequences of overlooking their difference.
In my view, the principal practical advantage of static type checking system (as implemented in current languages) is their ability to catch boundary conditions. Have you ever called a Python method and forgot that it might return None? Your program works fine for a while, but it will eventually trip because you forgot to test if the return value was None. It will probably just crash with an uncaught exception, but in the process may mangle or lose data. (Users tend not to like that. :)
In general, when boundary conditions are ignored, any degree of havoc can potentially result because your code is being interpreted in a way you never intended.
One answer is exception handling, and you can sometimes use this to salvage yourself from utter disaster, but if you are catching an exception that arose from a boundary condition you didn't think of, then your exception handling is too broad!
For typical programs written in a scripting language, the coder may actually want the program to just terminate on all unconsidered boundary cases. But when a script grows into a useful application (perhaps one that is run automatically by a cron job or a web server), it is eminently useful to have some sort of guarantee that it won't crash.
I have a separate email address for slashdot. And as soon as I submitted an article that was displayed on the front page and agreed to allow that email address to be publicly visible with the article announcement, I was suddenly flooded with spam. It looks like you missed out on a golden opportunity when you submitted your article without a link to your email. :)
I did some googling and found this opinion on the passage you mentioned.
Yeah, and then you can watch the cheap-ass power supply short out the first time you flip the switch, and fry your video card in the process. And trust me, you are not likely to be able to track down and get any reimbursement money for other damaged hardware out of a company that sells $35 cases. For the future, I do not plan on ever buying a generic power supply or another case that comes with a built-in power supply.