Then their "proof" seems to be based on a common misunderstanding, though. The halting problem only states that there is no algorithm that allows you to determine of any algorithm (including, notably, itself) that it will halt. It doesn't state that you cannot automatically proof that some specific algorithm (e.g. one for "ethical killing") will halt/is correct or that you cannot proof that most if not all algorithms we're interested in will halt/are correct. While many of the automated theorem provers are not fully automatic and may sometimes require you to choose a proof strategy, this has more to do with the complicated nature of the proofs (and incompleteness of HOL). There are also fully automated HOL theorem provers.
I believe most of the Airbus software based on Spark has been proved using automated theorem provers, but I might be wrong. Anyway, there are many automated correctness proofs for safety-critical software/hardware.
And just to make this clear, where I live you are allowed to lie to federal officers if you are accused, and there is no such crime as a 'conspiracy to lie to government investigators'. Not all countries are as fascist as the USA.
I did not reply to your first comment but to another one of your countless comments, namely one which was false. Before you pester public forums with your biased opinions on how to interpret idiotic laws, you should perhaps first learn how to argue.
Don't know why this has been modded funny, it just depends on the interpretation of "soon." Give it another hundred years and the solar system will indeed be crawling with private robots, unless we somehow manage to seriously fuck up our civilization until then. On a cosmic time scale another hundred or two hundred years is nothing.
What annoys me a bit, though, is that I'm probably born too early to be able to download my consciousness into a machine during my lifetime, so I won't see what the future brings.:(
- It has a faster executable startup time than Java and other languages that depend on the clunky JVM.
- It's not as OO-perverted as Java, or at least, allows you to write your OO-perverted code with less keystrokes than Java.
- It has many features that the Algol68 language has, too.
- It lacks many features that Common Lisp has and will never have them. (Whether you think that's good or not, depends a bit on the length of your beard and weather you primarily live off coke and chinese food and pizza or not.)
- It has built-in concurrency like Ada has, only that it is much less safe than Ada and also much slower.
- It is slower than C and Fortran, so if you do number crunching it will give you an additional coffee break.
- It provides endless opportunities and fun with fiddling around with glue code for interfacing to C and C++ libraries - like all new language!
- Its somewhat easier to learn and use than Forth, but less easier to use than Python (which is good, because we don't want it to be too easy now, do we)
Please notice that I'm not in any way affiliated with Google, so this not some hidden advertising/slashvertisement.
The ironic thing is that if there was a Microsoft Word for Linux and it could actually read its own file format correctly, then I would probably buy it just so I could exchange files with publishers without having to worry about missing special characters and malformed tables.
I believe him. Here my interpretation of what he said: "We share all bugs we find with large corporations except a small number of 0-day exploits for each system that we keep to ourselves and always up-to-date."
LOL, there are no anti-gay laws in Russia... except when they are cited explicitly by government officials as a reason for removing a statue of Steve Jobs because Tim Cook announced that he is gay. Let me guess, Russia didn't invade and illegaly annex the Crimea either?
I guess it's time for you to turn off your reality distortion field.
Nice troll post. Just about only real distinction between a professional and a hobby programmer is that the former gets paid whereas the latter doesn't. I've seen just as much complete crap written by professionals than has been written by so-called amateurs.
Besides, you're missing the point. Everybody should be able to program his computer in the way he or she likes and the tools should be easy to use and completely unrestricted. Nobody forces you to use someone else's program if you have no confidence in his or her abilities.
I agree. I used to program in REALbasic, it was extremely easy to get reasonably good results and I generally had a great time with it and sold lots of high quality shareware. (I know, I know, REALbasic was also responsible for a lot of low quality shareware, no doubt about that, but you will always get this with such a tool.) As long as you didn't stumble over one of the many implementation bugs it was a lot of fun and the fastest way to develop. This was long before it became ridiculously expensive, back in the time when Andrew spit out one great and slightly buggy free update after the other, and even longer before the name of the language was changed to some silly meaningless word that I have immediately forgotten after I first heard it.
I'm still looking for a decent substitute, even after I've switched to more complicated and equally excellent cross-platform languages like Racket. Python and Freepascal/Lazarus come closest to it but aren't nearly as easy to use and beginner friendly in my opinion.
Really? You can be required to sign something with your name in the US even if you don't want to? If that's true, then you're not living in a free country.
Well, it's about as critical as living under a government with whom you disagree. Sure, you could leave the country and live in the rainforests of Papua New Guinea for the rest of your life, so you have no right to complain about your government...
Slashdot Mirror
Then their "proof" seems to be based on a common misunderstanding, though. The halting problem only states that there is no algorithm that allows you to determine of any algorithm (including, notably, itself) that it will halt. It doesn't state that you cannot automatically proof that some specific algorithm (e.g. one for "ethical killing") will halt/is correct or that you cannot proof that most if not all algorithms we're interested in will halt/are correct. While many of the automated theorem provers are not fully automatic and may sometimes require you to choose a proof strategy, this has more to do with the complicated nature of the proofs (and incompleteness of HOL). There are also fully automated HOL theorem provers.
I believe most of the Airbus software based on Spark has been proved using automated theorem provers, but I might be wrong. Anyway, there are many automated correctness proofs for safety-critical software/hardware.
You mean satanist, right? The 'd' stands for daemon.
Nice non-sequitur.
And just to make this clear, where I live you are allowed to lie to federal officers if you are accused, and there is no such crime as a 'conspiracy to lie to government investigators'. Not all countries are as fascist as the USA.
I did not reply to your first comment but to another one of your countless comments, namely one which was false. Before you pester public forums with your biased opinions on how to interpret idiotic laws, you should perhaps first learn how to argue.
Its legal to lie to government investigators in your jurisdiction?
That's not what the guy was arrested for, dumbass.
Fascists.
Your laws are ridiculous.
Don't know why this has been modded funny, it just depends on the interpretation of "soon." Give it another hundred years and the solar system will indeed be crawling with private robots, unless we somehow manage to seriously fuck up our civilization until then. On a cosmic time scale another hundred or two hundred years is nothing.
What annoys me a bit, though, is that I'm probably born too early to be able to download my consciousness into a machine during my lifetime, so I won't see what the future brings. :(
- It's faster than Python and, I suppose, Ruby.
- It has a faster executable startup time than Java and other languages that depend on the clunky JVM.
- It's not as OO-perverted as Java, or at least, allows you to write your OO-perverted code with less keystrokes than Java.
- It has many features that the Algol68 language has, too.
- It lacks many features that Common Lisp has and will never have them. (Whether you think that's good or not, depends a bit on the length of your beard and weather you primarily live off coke and chinese food and pizza or not.)
- It has built-in concurrency like Ada has, only that it is much less safe than Ada and also much slower.
- It is slower than C and Fortran, so if you do number crunching it will give you an additional coffee break.
- It provides endless opportunities and fun with fiddling around with glue code for interfacing to C and C++ libraries - like all new language!
- Its somewhat easier to learn and use than Forth, but less easier to use than Python (which is good, because we don't want it to be too easy now, do we)
Please notice that I'm not in any way affiliated with Google, so this not some hidden advertising/slashvertisement.
5 years of Go versus 30 years of Common Lisp and 50 years of Lisp. :)
Please mod up. Seagate drives fail much sooner than all other brands.
The ironic thing is that if there was a Microsoft Word for Linux and it could actually read its own file format correctly, then I would probably buy it just so I could exchange files with publishers without having to worry about missing special characters and malformed tables.
You confuse the local laws of some countries with EU law.
Palemoon crashes a lot on my machine, Firefox doesn't ... which is weird, given that Palemoon is essentially a rebranded Firefox.
No, he doesn't, and neither do you.
Cake-cutting algorithms, I love them. I've read parts of the book by Robertson and Webb and always wonder about unusual and new applications for them.
There are plenty of nice things where I live (and on the Internet), so what the heck do you mean by "we can't have anything nice"? Care to explain?
I believe him. Here my interpretation of what he said: "We share all bugs we find with large corporations except a small number of 0-day exploits for each system that we keep to ourselves and always up-to-date."
LOL, there are no anti-gay laws in Russia ... except when they are cited explicitly by government officials as a reason for removing a statue of Steve Jobs because Tim Cook announced that he is gay. Let me guess, Russia didn't invade and illegaly annex the Crimea either?
I guess it's time for you to turn off your reality distortion field.
Nice troll post. Just about only real distinction between a professional and a hobby programmer is that the former gets paid whereas the latter doesn't. I've seen just as much complete crap written by professionals than has been written by so-called amateurs.
Besides, you're missing the point. Everybody should be able to program his computer in the way he or she likes and the tools should be easy to use and completely unrestricted. Nobody forces you to use someone else's program if you have no confidence in his or her abilities.
I agree. I used to program in REALbasic, it was extremely easy to get reasonably good results and I generally had a great time with it and sold lots of high quality shareware. (I know, I know, REALbasic was also responsible for a lot of low quality shareware, no doubt about that, but you will always get this with such a tool.) As long as you didn't stumble over one of the many implementation bugs it was a lot of fun and the fastest way to develop. This was long before it became ridiculously expensive, back in the time when Andrew spit out one great and slightly buggy free update after the other, and even longer before the name of the language was changed to some silly meaningless word that I have immediately forgotten after I first heard it.
I'm still looking for a decent substitute, even after I've switched to more complicated and equally excellent cross-platform languages like Racket. Python and Freepascal/Lazarus come closest to it but aren't nearly as easy to use and beginner friendly in my opinion.
It could be a spy satellite and space junk at the same time. Perhaps the Russians like irony.
Really? You can be required to sign something with your name in the US even if you don't want to? If that's true, then you're not living in a free country.
Well, it's about as critical as living under a government with whom you disagree. Sure, you could leave the country and live in the rainforests of Papua New Guinea for the rest of your life, so you have no right to complain about your government ...