You have to knowingly and willfully help someone infringe. It's not a double standard--just as you are being facetious about things that would probably never be considered infringement, a judge would probably throw those out. But making files available in a file sharing app is obviously a deliberate act intended to allow people to copy them. And that's probably illegal under current copyright law.
I'm not a fan of the copyright law, but it's really not as vague (ignoring the DMCA ammendments) as you guys seem to make it out to be!
You should take a break and read the copyright code. (Just search for "17 USC" on google.) There are all sorts of exemptions for "incidental" copies, such as the ones made when you play a CD in a digital player.
The complaintant would have to prove that the user did it on purpose. If he really just installed windows and it started ripping his CDs and putting them online, and he really didn't know that, then he'd probably be ok. (In fact, Napster used to search your whole hard drive by default, right?) But my bet is that most of these people did it on purpose, and that shouldn't be too hard to prove.
> How do we determine which of these products are necessary enough for other tasks that the manufacturer is not to blame for > the way they are used?
We read the law, and where the law is unclear, consult a judge.
> If Napster was commonly used for legitimate purposes, would it still be around today?
Probably. It also would have helped if they didn't have internal memos indicating that they knew about and encouraged piracy for financial benefit.
Personally, I am not a fan of copyright law in general, and would be happy if Napster was still running. I think it's morally defensible to share data with your friends. But the law is filled with grey areas, and outlawing something like Napster does NOT mean that we have to outlaw computers and hard disks in order to be consistent. (It's the same as outlawing machineguns but not archery sets, and PCP but not caffeine.)
Um, why do you think napster was shut down? Do you not believe that contributory infringement is illegal?
In order to be guilty you have to be knowingly and willfully involved in the copying. This, as far as I know, is the main thing that defines contributory infringement, and it's a clear distinction between sharing on a P2P network and selling a photocopier. Copy machines at places like Kinko's and libraries often do have little placards (if just for show) warning you about copyright violation. Similarly, if you brought in a Harry Potter novel and asked them to make a jillion copies of it, they wouldn't.
I don't like copyright law very much, but it *is* law, and it is not as incomprehensibly illogical as you think.
OK, but you have to stop calling it "stealing." It's copyright infringement, not stealing. Stealing is where you take physical property, and then the original owner doesn't have it any more.
By making it so easy to copy the files, you would certainly be in danger of contributory infringement. That means, even though it's others that are doing the copying, you're still liable because you knowingly put them online. Contributory infringement is what got Napster.
If these guys think they haven't already compromised their "art" to appear on the radio, sell millions of albums/singles, and tour with laser light shows, then they are fucken nuts. Of course, they're free to put whatever draconian licensing schemes on their music they want, and I hope they do, because it will eventually drive consumers away from giving money to the RIAA and its bedfellows.
Yeah, several of the legal threats I've received in the past have signed off with "Very truly yours." I like to write back with "Extremely truly yours.";)
They certainly don't have to comply with Marvel's demands, and Marvel probably won't do anything if they do. But they've already almost certainly violated copyright/trademark law, so even if they pull the stuff now Marvel can still sue them. That's the leverage that Marvel is threatening to use unless they get those names.
If you have 'collapse sections' turned on, then you're going to see all of games.slashdot.org interspersed with the main articles, along with ask slashdot, etc. You can tell because they say Games: in front of them.
Yes, there is. Rice's theorem proves it impossible in the general case.
You are misapplying the theorem, or else don't understand what it says. There are systems where given a program, and a proof, verification of non-trivial properties (like termination) is decidable. Yes, there is no program that will generate that proof for you for arbitrary programs and properties. But that does not mean that a human (or even, sometimes, a computer) can't create a proof for a specific program and then verify that proof mechanically. People do that every day, and it does not mean that the properties are trivial, either in the Rice sense or the practical sense.
The argument you're making is essentially identical to, "The undecidability of the halting problem tells us that writing programs is hopeless." Making general program-writing tools (input spec, output program) is hopeless, yes, but that does not mean that we can't make lots of useful specific programs.
I'd go on, but this is already below the front page fold by five or ten pages, so who'd read it anyway?
In fact this sort of proof is one of the reasons I seriously wonder why so many people still seem to be pursuing this.
Well, for starters, many systems (I don't know much about Z) don't work this way. They have the programmer write a proof with his code, and that proof system is such that the proofs are easy to validate. What is sacrificed is the ability to write some correct programs in ways that the proof system can't comprehend, but for the most part if you're trying to write clear, maintainable code, you don't want to write the program that way either. (For instance, if you're going to write a little turing machine evaluator in your program to do some of the work, these kinds of systems are going to have a lot of trouble with that.)
Also, just because something is impossible to do in general doesn't mean that it isn't easy or useful to do in specific cases. For instances, using your same argument we know that it is impossible to write programs, in general. (Write the spefication for your program-verifying program, or just write the halting problem down.) But of course we write programs all of the time!
no such language can exist, unless it is trivial and the correctness criterion is trivial.
True, but I think the word "trivial" is pretty misleading here. There are many programming languages with built-in safety properties (SML and Java for instance), where you simply cannot write programs that corrupt memory, execute arbitrary code (ie, through buffer overflows), etc. (Note: this is a property of the language. Java is often compiled to a VM, SML is usually not, but that has nothing to do with their safety properties.) That safety property is "trivial" by your argument, but I think it is a damn useful one.
Unit testing is great for testing the common use-cases of business software. I program in academic safe languages every day, and I still use unit testing. But unit testing can't really catch security holes like buffer overflows (and security misdesigns like protocol errors), and it can't really assure perfect operation in life-critical systems (I know for a fact that BMW uses model checking to verify their drive-by-wire systems work properly). Mathematical proofs are good for catching these corner cases, and though they are probably dozens of years away from being mainstream, I do think they'll get there.
It's not a supercomputing thing, it's just tedious. Verification of a proof is usually really fast. The thing is, it's not "practicall impossible" at all... in fact, it's often very easy. But it is something that has so little benefit over an informal proof that nobody does it for practical software. Sorry if I sounded harsh, but there are a lot of people posting to this story that totally don't understand the mathematics involved or even what they're trying to do, and that drives me nuts.;)
I'm not wrong. What the original poster said is that it's impossible to prove anything but the simplest algorithms correct. That's not true at all; people publish papers with complicated algorithms and proofs of their correctness every day. Those proofs of correctness can usually be concretized to the source code level, it's just painful. It is not impossible! (There is no limit to finite state spaces. Haven't you ever heard of induction??)
I'm not talking about a computer program that examines raw source code and tells you wether it is correct or not, so your other "proof" doesn't apply. I'm not talking about model checking (that's what you seem to describe above), which can be useful, but not usually for *algorithm* analysis. I'm talking about writing down a proof of correctness, and perhaps checking that proof with a computer.
I happen to think these kinds of methods are not practical today (though they can lead to type systems that are practical). But there is certainly no theorem telling us that it's hopeless.
I vaguely remember that short of an exhaustive date set test, it's actually IMPOSSIBLE to determine mathematically that an algorithm is correct for any but the simplest (read shortest) pieces of code.
This is total crap. You can, of course, prove algorithms of any size correct. Some really long (textually) algorithms can be easy to prove, and some really short ones, like this:/* terminate and return 1 for any positive input */ int collatz(int i) {
if (i & 1) return collatz (i * 3 + 1);
else return collatz(i >> 1); }... are really, really hard to prove correct. In general, it's not feasible to prove big pieces of practical code correct using techniques like these, but with suitable abstraction it can be a helpful part of the engineering process. In any case, it is definitely not impossible.
Yeah, and get ready for me not buying it. The price of console games has been getting awful! Personally, I just live a year or two behind the new release schedule, and get games out of the bargain/used section for much cheaper.
Too many gadgets crowding out my ''shame''
on
Robots Without a Cause
·
· Score: 2, Informative
Well, maybe he's right. But I must say that as far as problems go, this is a pretty good one to have.
(By the way, when electricity was first discovered, it was mostly used to amuse people by shocking them.)
You can use line numbers in QBasic. Of course, the reason to remove them is that it becomes impossible to maintain your code when you've got lines 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, and need to insert a line between 64 and 65.;)
For what it's worth, I learned on QBasic and think it was a really good starting point.
GameBoy is for 10-year-olds. If you're 20 or 25 years old, it's probably not a good idea to draw a GameBoy out of your pocket on a Friday night in a public place.
> I think when you get down to the nitty gritty language implmentation most languages implement it as a macro with labels and > goto.
Yeah, well, that's how functions are implemented too.
> What this boils down to is that you need a new keyword to tell the compiler your passed function+environment will be stack > allocated or heap allocated.
You're right, if while lives in a different module and your module system only lets you specify the most basic things about the symbol. But lots of compilers do cross-module optimizations, and in this case a proper leaf procedure where the argument functions don't escape (like the original implementation of while) could be called with pointers to closures on the stack without any problem.
> Where "(\ ()...)" is my made-up syntax for introducing a function of 0 arguments with "..." as its body.
Why not make up a simpler syntax, then? You could use a single character for suspending code with zero arguments, and then the use of the while example would be only two characters longer than the lisp macro version. (Lisp programmers surely cannot complain about two extra characters, as their language is filled with extra verbosity!)
The advantage of such a system is that it can be explained simply in terms of other features in the language, and so it behaves rationally. You can't incur capture or otherwise violate the scope of variables (except in the ways that lisp already does), you can't change around the code that is passed in (except in the normal lisp way, again) and most importantly a programmer can look at a piece of code and know "what it does" at the same level as he looks at other code. For the uses of macros that I think of as good coding practice, this is certainly possible.
> This approach is what I'd call "too dang inconvenient".:) I think history bears me out that macros are the superior > approach, as most languages do NOT implement while as a function.;)
Well, most languages also do not implement it as a macro. As a lisp programmer, do you REALLY want to argue that the popular historic ways is the superior way? (In fairness, I think you have a good argument, but this isn't it!!)
> Also there's an efficiency argument to be made against passing too many functions with "closed variables", as this will often > cause those variables to be heap allocated instead of (faster) stack allocated. On the other hand 99% of the time you've got > a fast enough computer to not care, but I have had times where the efficiency matters.
I don't know what "closed variables" means; do you mean an environment? Who says a compiler has to heap-allocate closures? There is an efficiency issue, sure, but this is not something that the programmer should have to deal with. A good optimizer should be able to tell that inlining the 'while' function turns its arguments into beta-redices, and then you end up with the same code that the macro pre-compiler produces.
> I don't think you can do this by passing around functions.
No, because this is precisely the kind of hack that makes lexically-scoped functions nice and macros unhygienic!;)
Slashdot Mirror
You have to knowingly and willfully help someone infringe. It's not a double standard--just as you are being facetious about things that would probably never be considered infringement, a judge would probably throw those out. But making files available in a file sharing app is obviously a deliberate act intended to allow people to copy them. And that's probably illegal under current copyright law.
I'm not a fan of the copyright law, but it's really not as vague (ignoring the DMCA ammendments) as you guys seem to make it out to be!
You should take a break and read the copyright code. (Just search for "17 USC" on google.) There are all sorts of exemptions for "incidental" copies, such as the ones made when you play a CD in a digital player.
The complaintant would have to prove that the user did it on purpose. If he really just installed windows and it started ripping his CDs and putting them online, and he really didn't know that, then he'd probably be ok. (In fact, Napster used to search your whole hard drive by default, right?) But my bet is that most of these people did it on purpose, and that shouldn't be too hard to prove.
> How do we determine which of these products are necessary enough for other tasks that the manufacturer is not to blame for
> the way they are used?
We read the law, and where the law is unclear, consult a judge.
> If Napster was commonly used for legitimate purposes, would it still be around today?
Probably. It also would have helped if they didn't have internal memos indicating that they knew about and encouraged piracy for financial benefit.
Personally, I am not a fan of copyright law in general, and would be happy if Napster was still running. I think it's morally defensible to share data with your friends. But the law is filled with grey areas, and outlawing something like Napster does NOT mean that we have to outlaw computers and hard disks in order to be consistent. (It's the same as outlawing machineguns but not archery sets, and PCP but not caffeine.)
Um, why do you think napster was shut down? Do you not believe that contributory infringement is illegal?
In order to be guilty you have to be knowingly and willfully involved in the copying. This, as far as I know, is the main thing that defines contributory infringement, and it's a clear distinction between sharing on a P2P network and selling a photocopier. Copy machines at places like Kinko's and libraries often do have little placards (if just for show) warning you about copyright violation. Similarly, if you brought in a Harry Potter novel and asked them to make a jillion copies of it, they wouldn't.
I don't like copyright law very much, but it *is* law, and it is not as incomprehensibly illogical as you think.
OK, but you have to stop calling it "stealing." It's copyright infringement, not stealing. Stealing is where you take physical property, and then the original owner doesn't have it any more.
By making it so easy to copy the files, you would certainly be in danger of contributory infringement. That means, even though it's others that are doing the copying, you're still liable because you knowingly put them online. Contributory infringement is what got Napster.
If these guys think they haven't already compromised their "art" to appear on the radio, sell millions of albums/singles, and tour with laser light shows, then they are fucken nuts. Of course, they're free to put whatever draconian licensing schemes on their music they want, and I hope they do, because it will eventually drive consumers away from giving money to the RIAA and its bedfellows.
My favorite thing about these games was the music, by Hiro Tanaka (Metroid, Kid Icarus). Is that guy still making video game music??
Yeah, several of the legal threats I've received in the past have signed off with "Very truly yours." I like to write back with "Extremely truly yours." ;)
They certainly don't have to comply with Marvel's demands, and Marvel probably won't do anything if they do. But they've already almost certainly violated copyright/trademark law, so even if they pull the stuff now Marvel can still sue them. That's the leverage that Marvel is threatening to use unless they get those names.
If you have 'collapse sections' turned on, then you're going to see all of games.slashdot.org interspersed with the main articles, along with ask slashdot, etc. You can tell because they say Games: in front of them.
(?)
The specification is right in the comment before the code. It says that it returns 1 for any positive input.
Yes, there is. Rice's theorem proves it impossible in the general case.
You are misapplying the theorem, or else don't understand what it says. There are systems where given a program, and a proof, verification of non-trivial properties (like termination) is decidable. Yes, there is no program that will generate that proof for you for arbitrary programs and properties. But that does not mean that a human (or even, sometimes, a computer) can't create a proof for a specific program and then verify that proof mechanically. People do that every day, and it does not mean that the properties are trivial, either in the Rice sense or the practical sense.
The argument you're making is essentially identical to, "The undecidability of the halting problem tells us that writing programs is hopeless." Making general program-writing tools (input spec, output program) is hopeless, yes, but that does not mean that we can't make lots of useful specific programs.
I'd go on, but this is already below the front page fold by five or ten pages, so who'd read it anyway?
I will.
In fact this sort of proof is one of the reasons I seriously wonder why so many people still seem to be pursuing this.
Well, for starters, many systems (I don't know much about Z) don't work this way. They have the programmer write a proof with his code, and that proof system is such that the proofs are easy to validate. What is sacrificed is the ability to write some correct programs in ways that the proof system can't comprehend, but for the most part if you're trying to write clear, maintainable code, you don't want to write the program that way either. (For instance, if you're going to write a little turing machine evaluator in your program to do some of the work, these kinds of systems are going to have a lot of trouble with that.)
Also, just because something is impossible to do in general doesn't mean that it isn't easy or useful to do in specific cases. For instances, using your same argument we know that it is impossible to write programs, in general. (Write the spefication for your program-verifying program, or just write the halting problem down.) But of course we write programs all of the time!
no such language can exist, unless it is trivial and the correctness criterion is trivial.
True, but I think the word "trivial" is pretty misleading here. There are many programming languages with built-in safety properties (SML and Java for instance), where you simply cannot write programs that corrupt memory, execute arbitrary code (ie, through buffer overflows), etc. (Note: this is a property of the language. Java is often compiled to a VM, SML is usually not, but that has nothing to do with their safety properties.) That safety property is "trivial" by your argument, but I think it is a damn useful one.
Unit testing is great for testing the common use-cases of business software. I program in academic safe languages every day, and I still use unit testing. But unit testing can't really catch security holes like buffer overflows (and security misdesigns like protocol errors), and it can't really assure perfect operation in life-critical systems (I know for a fact that BMW uses model checking to verify their drive-by-wire systems work properly). Mathematical proofs are good for catching these corner cases, and though they are probably dozens of years away from being mainstream, I do think they'll get there.
Oops, it should return 1 if the input is 1, sorry.
It's not a supercomputing thing, it's just tedious. Verification of a proof is usually really fast. The thing is, it's not "practicall impossible" at all... in fact, it's often very easy. But it is something that has so little benefit over an informal proof that nobody does it for practical software. Sorry if I sounded harsh, but there are a lot of people posting to this story that totally don't understand the mathematics involved or even what they're trying to do, and that drives me nuts. ;)
I'm not wrong. What the original poster said is that it's impossible to prove anything but the simplest algorithms correct. That's not true at all; people publish papers with complicated algorithms and proofs of their correctness every day. Those proofs of correctness can usually be concretized to the source code level, it's just painful. It is not impossible! (There is no limit to finite state spaces. Haven't you ever heard of induction??)
I'm not talking about a computer program that examines raw source code and tells you wether it is correct or not, so your other "proof" doesn't apply. I'm not talking about model checking (that's what you seem to describe above), which can be useful, but not usually for *algorithm* analysis. I'm talking about writing down a proof of correctness, and perhaps checking that proof with a computer.
I happen to think these kinds of methods are not practical today (though they can lead to type systems that are practical). But there is certainly no theorem telling us that it's hopeless.
I vaguely remember that short of an exhaustive date set test, it's actually IMPOSSIBLE to determine mathematically that an algorithm is correct for any but the simplest (read shortest) pieces of code.
/* terminate and return 1 for any positive input */ ... are really, really hard to prove correct. In general, it's not feasible to prove big pieces of practical code correct using techniques like these, but with suitable abstraction it can be a helpful part of the engineering process. In any case, it is definitely not impossible.
This is total crap. You can, of course, prove algorithms of any size correct. Some really long (textually) algorithms can be easy to prove, and some really short ones, like this:
int collatz(int i) {
if (i & 1) return collatz (i * 3 + 1);
else return collatz(i >> 1);
}
> "Get ready for $60 Halo II."
Yeah, and get ready for me not buying it. The price of console games has been getting awful! Personally, I just live a year or two behind the new release schedule, and get games out of the bargain/used section for much cheaper.
Well, maybe he's right. But I must say that as far as problems go, this is a pretty good one to have.
(By the way, when electricity was first discovered, it was mostly used to amuse people by shocking them.)
Someone with a bunch of bandwidth (sourceforge?) definitely should do it. I'd be happy to contribute my game data from days past...
You can use line numbers in QBasic. Of course, the reason to remove them is that it becomes impossible to maintain your code when you've got lines 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, and need to insert a line between 64 and 65. ;)
For what it's worth, I learned on QBasic and think it was a really good starting point.
GameBoy is for 10-year-olds. If you're 20 or 25 years old, it's probably not a good idea to draw a GameBoy out of your pocket on a Friday night in a public place.
Nokia, I am not afraid!!
> I think when you get down to the nitty gritty language implmentation most languages implement it as a macro with labels and
> goto.
Yeah, well, that's how functions are implemented too.
> What this boils down to is that you need a new keyword to tell the compiler your passed function+environment will be stack
> allocated or heap allocated.
You're right, if while lives in a different module and your module system only lets you specify the most basic things about the symbol. But lots of compilers do cross-module optimizations, and in this case a proper leaf procedure where the argument functions don't escape (like the original implementation of while) could be called with pointers to closures on the stack without any problem.
> Where "(\ () ...)" is my made-up syntax for introducing a function of 0 arguments with "..." as its body.
:) I think history bears me out that macros are the superior ;)
;)
Why not make up a simpler syntax, then? You could use a single character for suspending code with zero arguments, and then the use of the while example would be only two characters longer than the lisp macro version. (Lisp programmers surely cannot complain about two extra characters, as their language is filled with extra verbosity!)
The advantage of such a system is that it can be explained simply in terms of other features in the language, and so it behaves rationally. You can't incur capture or otherwise violate the scope of variables (except in the ways that lisp already does), you can't change around the code that is passed in (except in the normal lisp way, again) and most importantly a programmer can look at a piece of code and know "what it does" at the same level as he looks at other code. For the uses of macros that I think of as good coding practice, this is certainly possible.
> This approach is what I'd call "too dang inconvenient".
> approach, as most languages do NOT implement while as a function.
Well, most languages also do not implement it as a macro. As a lisp programmer, do you REALLY want to argue that the popular historic ways is the superior way? (In fairness, I think you have a good argument, but this isn't it!!)
> Also there's an efficiency argument to be made against passing too many functions with "closed variables", as this will often
> cause those variables to be heap allocated instead of (faster) stack allocated. On the other hand 99% of the time you've got
> a fast enough computer to not care, but I have had times where the efficiency matters.
I don't know what "closed variables" means; do you mean an environment? Who says a compiler has to heap-allocate closures? There is an efficiency issue, sure, but this is not something that the programmer should have to deal with. A good optimizer should be able to tell that inlining the 'while' function turns its arguments into beta-redices, and then you end up with the same code that the macro pre-compiler produces.
> I don't think you can do this by passing around functions.
No, because this is precisely the kind of hack that makes lexically-scoped functions nice and macros unhygienic!