Parent is indeed Insightful. This is exactly the kind of argument that I (licensing-overeducated, IP-overeducated, slashdot-junkie free software zealot) have seen a thousand times, and can recite when waken up at night. It is very insightful for those who must still be enlightened on these topics.
You know what would I like to see in Slashcode? A "insightful for newbies, redundant for zealots +0" qualifier. Then I would set my reason-modifier for this qualifier to -6. Voila, no more insightful, but for me totally redundant posts in sight.
We live in an era where really interesting theorems often have many hundred or thousand pages proofs. (Last Fermat by Wiles, Kepler by Hales, The Classification of Simple Groups). It's unrealistic to believe that there are no gaps in such proofs. All my three example theorems had gaps, some quite serious. A huge gap in the proof of the Classification of Simple Groups was only found after about ten years. Serre, the most prominent group theorist still doesn't believe that the theorem is really proved.
So, it's unrealistic to believe that there are no gaps in very long proofs UNLESS the proofs are totally formalized. My prediction is that in 20 years, only such formalized proofs will be accepted in journals on pure mathematics.
There are now three different proofs of the Theorem. All work by by exhaustion of a very large problem space. The original '77 proof is by Appel and Haken. A second one is by Seymour et al. The third one by Georges Gonthier is very new. It's the really interesting one in this discussion, because it is a totally formalized proof, built with the help of the Coq mechanical theorem prover.
The point is, IF you believe that the Coq software works correctly, then you can now be SURE about the Four Color Theorem. Before Gonthier, you had to proof-check hudreds of pages, and debug and run some quite complicated programs to validate the proof. Seymour et al. did their own proof partly because this was easier than verifying Appel and Haken's very complicated one.
The problem with human-made proofs is that there can be gaps and even faults in them. Proofs with hundreds of pages are full of sentences starting with "It's easy to see that X.". Most often X is indeed obviously true, sometimes it is not.
The goal of computer-aided theorem proving is to eliminate all these gaps. The human prover sketches her proof for the computer in a formal language. If some steps are missing, the computer calls her attention to these. When the long interactive process is finished, we have a proof that does not have any ""It's easy to see"s and "Obviously"s in it. At this point, another human can check the proof. But there is really no good reason to believe that this other human is more adept at checking it than the computer itself.
The proof of the Four Color Theorem was recently formalized by Georges Gonthier in this way.
From a philosophical point of view, many arguments can be made. But from a practical point of view: If I have to choose between believing a 300 pages long proof written in an informal language (Fermat's Last Theorem by Wiles) and a 1000 pages long proof written in a formal language, verified by a computer, I will choose the second one anytime.
Don't fuck with the Hawkman, 'cause the Hawkman ain't down with that eye for an eye bullshit. Fuck that! You take an eye and I'll take your motherfucking head!
(From "All My Shootin's Be Drivebys" by MC Hawking)
How do we KNOW that there is no DNA copy? Isn't it possible that the DNA copy is not word-for-word? Maybe some trivial bijective transformation is applied, and the repair mechanism decodes this transformation when it corrects the original. Could we find the DNA copy even if this is the case?
...I finally managed to RTFA, and my question is still very valid.
"A mutated gene can be put right by various mechanisms that are already known, but all require a correct copy of the gene to be available to serve as the template. The Purdue team scanned the DNA of the entire arabidopsis genome for a second, cryptic copy of the hothead gene but could find none."
So isn't it more plausible that they didn't search hard enough, or that the copy is more cryptic than they imagined? This second case would still make a quite interesting discovery, but it wouldn't involve RNA.
How do we KNOW that there is no DNA copy? Isn't it possible that the DNA copy is not word-for-word? Maybe some trivial bijective transformation is applied, and the repair mechanism decodes this transformation when it corrects the original. Could we find the DNA copy even if this is the case?
"Do they read those from Project Gutenberg? I'm not sure how many do."
Me neither. But I'm very grateful for Project Gutenberg, because it is the basis of our open source Hungarian-English parallel text database. Thsi, in turn, helps us semi-automatically build a broad open source Hungarian-English dictionary. In essence, Project Gutenberg is invaluable for developing open source computational lingustics technology.
Yeah. I just did this trick with a deck reduced to numbers 2 to 9. (Modulo 10 arithmetics is easier.) I managed to deeply impress my non-geek girlfriend.
A small case study: Once I made a small addition to an article. It stayed there for a month, intact. Then people started to edit it to make it sound better in English. (I'm not a native English speaker.) But these people definitely didn't understand the topic, so soon my addition was modified to some better-sounding, but factually totally incorrect mess. When I realized this, I got angry, and trolled on the discussion page. I also corrected the mistakes. In an hour, some competent and nice person arrived. He verified my statements, improved my corrections' grammar, added some more material, thanked me for my help, and politely asked me not to indulge in personal attacks. It was really smooth and professional.
Re:Major Features Dropped From GCC 4.0
on
GCC 4.0 Preview
·
· Score: 1
Politics is what's preventing us from considering LLVM, let alone the long and torturous process of making the code work. The brutally short story is that GCC is operating under a certain restriction imposed by RMS since its inception, and LLVM -- or really, any good whole-program optimization technique -- would require us to violate that restriction.
Would you tell us some more about this restriction? Is it a legal or a technological one? I'm very curious. Thanks in advance.
It isn't a big deal. Instead of "Mars Rovers Have Incorrect Instruments Installed", a better headline would have been "Mars Rover Data Analyzed With Incorrect Calibration Data Files". But the editors would have rejected a headline like that.
You made me understand an important thing about Slashdot: I always blamed the editors for accepting misleadingly sensationalist headlines. Now I see that these are the results of a darwinistic arms race fought for the attention of the editors.
On the other hand, I still blame the editors for accepting all those flamebait articles. And I didn't even talk about Roland Piquepaille.
This is news of '93, when Brown et al. at IBM built their famous statistical machine translation system. It does exactly what is described in the article. I myself work on such a system (for Hungarian-to-English translation).
The article (press release?) is totally misleading. Kevin Knight and Daniel Marcu are building on at least 15 years of active research on statistical machine translation. On the other hand, they are really very good at it.
He didn't talk about a very interesting question: How many of the KDE contibutors work on KDE as their day job? Or more importantly: how much of the KDE codebase is a work of people as their day job?
In the case of Linux, I think currently all of the most important contributors (who, on the whole, are responsible for almost all of the incoming core code) are now getting paid for their work on Linux (at OSDL, Red Hat, SUSE, IBM etc.). The same is true for Mozilla (Mozilla Foundation, Oracle, IBM, and now, famously, Google). Of course, this wasn't always so. Anyway, what's the case with KDE?
Just to state the obvious, I'll just give a rebuttal to some of these statements.
"Installing Firefox requires downloading an unsigned binary from a random web server"
It's a web server that mozilla.org directs you to. If you're downloading Firefox, you need to trust mozilla.org. Likewise, if you're downloading Internet Explorer, you need to trust microsoft.com.
This rebruttal is not working, unfortunately. The maintainers of the random webserver can change the content of the mirror to malicious code.
This is the third or fouth time that someone points to faser.net/mab on this thread as an example of a good XUL application. No other examples mentioned at Score:5. That thing is very-very cool indeed. But I'd really like to know why aren't there many more of these.
Please mod parent UP. This is the most insightful remark on time travel I have ever read. And I read a lot. 808140, please recommend some further reading.:)
I really liked your explanation about scientists answering why-questions with how-answers. But let me mention a possible point where science gives a why-answer in this sense. The Anthropic Principle is generally frowned upon, because the answer it gives is unsatisfying and can even be considered nihilistic. But it is a why-answer.
"Customers that do web application development heavily use DHTML and other special features that Konqueror doesn't handle very well and it is a lot of work to implement this. Although I like KHTML and the architecture quite a bit I am sad to say that probably the Gecko rendering engine will be the dominant one used in the enterprise arena, and as KDE developers we've got to make sure that we can integrate Gecko fairly well into KDE.
So Lars Knoll and Zack Rusin started working on this at aKademy and I was delighted when they put me aside and showed me what they have done in just three days. It is amazing! I think it is the right way to go! It is a bit sad for KHTML and I hope that despite this people will still maintain it as it is a nice lightweight browser. If it would be a purely technical decision, KHTML has the better architecture, but sometimes you need to go the shortest way to get to your target."
Why is it just as unlikely? Would there be any interesting consequences if NP=co-NP? It doesn't help resolve the P=NP question.
I'll give two different answers. Neither will be fully convincing.
1. Some of the most interesting mathematical theorems have this form: "The existence of an object and the nonexistence of another object are logically equivalent." Linear algebra and linear programming duality, the Nullstellensatz and the theory of matchings are nice examples of this. NP=co-NP would mean that we automatically get such theorems for any possible NP search question, like the existence of cliques, satisfying assingments and so on.
2. Both P=NP and NP=co-NP are stronger versions of "the polynomial hierarchy collapses" statement. Speaking in metaphors, P=NP says that "every imaginable bounded-round two-player game is easy to play". NP=co-NP says that "every imaginable bounded-round two-player game is as easy as solitaire". The collapse statement says something like "many-round two-player games are no harder than k-round two-player games, for some fixed k." Even this much weaker statement is considered very unlikely by computer scientists.
Slashdot Mirror
Parent is indeed Insightful. This is exactly the kind of argument that I (licensing-overeducated, IP-overeducated, slashdot-junkie free software zealot) have seen a thousand times, and can recite when waken up at night. It is very insightful for those who must still be enlightened on these topics.
You know what would I like to see in Slashcode? A "insightful for newbies, redundant for zealots +0" qualifier. Then I would set my reason-modifier for this qualifier to -6. Voila, no more insightful, but for me totally redundant posts in sight.
We live in an era where really interesting theorems often have many hundred or thousand pages proofs. (Last Fermat by Wiles, Kepler by Hales, The Classification of Simple Groups). It's unrealistic to believe that there are no gaps in such proofs. All my three example theorems had gaps, some quite serious. A huge gap in the proof of the Classification of Simple Groups was only found after about ten years. Serre, the most prominent group theorist still doesn't believe that the theorem is really proved.
So, it's unrealistic to believe that there are no gaps in very long proofs UNLESS the proofs are totally formalized. My prediction is that in 20 years, only such formalized proofs will be accepted in journals on pure mathematics.
There are now three different proofs of the Theorem. All work by by exhaustion of a very large problem space. The original '77 proof is by Appel and Haken. A second one is by Seymour et al. The third one by Georges Gonthier is very new. It's the really interesting one in this discussion, because it is a totally formalized proof, built with the help of the Coq mechanical theorem prover.
The point is, IF you believe that the Coq software works correctly, then you can now be SURE about the Four Color Theorem. Before Gonthier, you had to proof-check hudreds of pages, and debug and run some quite complicated programs to validate the proof. Seymour et al. did their own proof partly because this was easier than verifying Appel and Haken's very complicated one.
There is a very nice article about this here.
The problem with human-made proofs is that there can be gaps and even faults in them. Proofs with hundreds of pages are full of sentences starting with "It's easy to see that X.". Most often X is indeed obviously true, sometimes it is not.
The goal of computer-aided theorem proving is to eliminate all these gaps. The human prover sketches her proof for the computer in a formal language. If some steps are missing, the computer calls her attention to these. When the long interactive process is finished, we have a proof that does not have any ""It's easy to see"s and "Obviously"s in it. At this point, another human can check the proof. But there is really no good reason to believe that this other human is more adept at checking it than the computer itself.
The proof of the Four Color Theorem was recently formalized by Georges Gonthier in this way.
From a philosophical point of view, many arguments can be made. But from a practical point of view: If I have to choose between believing a 300 pages long proof written in an informal language (Fermat's Last Theorem by Wiles) and a 1000 pages long proof written in a formal language, verified by a computer, I will choose the second one anytime.
Don't fuck with the Hawkman, 'cause the Hawkman ain't down with that eye for an eye bullshit.
Fuck that! You take an eye and I'll take your motherfucking head!
(From "All My Shootin's Be Drivebys" by MC Hawking)
"A mutated gene can be put right by various mechanisms that are already known, but all require a correct copy of the gene to be available to serve as the template. The Purdue team scanned the DNA of the entire arabidopsis genome for a second, cryptic copy of the hothead gene but could find none."
So isn't it more plausible that they didn't search hard enough, or that the copy is more cryptic than they imagined? This second case would still make a quite interesting discovery, but it wouldn't involve RNA.
How do we KNOW that there is no DNA copy? Isn't it possible that the DNA copy is not word-for-word? Maybe some trivial bijective transformation is applied, and the repair mechanism decodes this transformation when it corrects the original. Could we find the DNA copy even if this is the case?
"Do they read those from Project Gutenberg? I'm not sure how many do."
Me neither. But I'm very grateful for Project Gutenberg, because it is the basis of our open source Hungarian-English parallel text database. Thsi, in turn, helps us semi-automatically build a broad open source Hungarian-English dictionary. In essence, Project Gutenberg is invaluable for developing open source computational lingustics technology.
Yeah. I just did this trick with a deck reduced to numbers 2 to 9. (Modulo 10 arithmetics is easier.) I managed to deeply impress my non-geek girlfriend.
A small case study: Once I made a small addition to an article. It stayed there for a month, intact. Then people started to edit it to make it sound better in English. (I'm not a native English speaker.) But these people definitely didn't understand the topic, so soon my addition was modified to some better-sounding, but factually totally incorrect mess. When I realized this, I got angry, and trolled on the discussion page. I also corrected the mistakes. In an hour, some competent and nice person arrived. He verified my statements, improved my corrections' grammar, added some more material, thanked me for my help, and politely asked me not to indulge in personal attacks. It was really smooth and professional.
Politics is what's preventing us from considering LLVM, let alone the long and torturous process of making the code work. The brutally short story is that GCC is operating under a certain restriction imposed by RMS since its inception, and LLVM -- or really, any good whole-program optimization technique -- would require us to violate that restriction.
Would you tell us some more about this restriction? Is it a legal or a technological one? I'm very curious. Thanks in advance.
Somewhat related to the branding question, another Mozilla problem:
RMS wants to rebrand Firefox.
This thing will surely appear soon as another sensationalist Slashdot headline.
It isn't a big deal. Instead of "Mars Rovers Have Incorrect Instruments Installed", a better headline would have been "Mars Rover Data Analyzed With Incorrect Calibration Data Files". But the editors would have rejected a headline like that.
You made me understand an important thing about Slashdot: I always blamed the editors for accepting misleadingly sensationalist headlines. Now I see that these are the results of a darwinistic arms race fought for the attention of the editors.
On the other hand, I still blame the editors for accepting all those flamebait articles. And I didn't even talk about Roland Piquepaille.
It wasn't Kapor who said this, it was the interviewer.
This is news of '93, when Brown et al. at IBM built their famous statistical machine translation system. It does exactly what is described in the article. I myself work on such a system (for Hungarian-to-English translation).
The article (press release?) is totally misleading. Kevin Knight and Daniel Marcu are building on at least 15 years of active research on statistical machine translation. On the other hand, they are really very good at it.
I'd like to moderate parent "Don't read any other posts on this thread, this is the only important one".
He didn't talk about a very interesting question: How many of the KDE contibutors work on KDE as their day job? Or more importantly: how much of the KDE codebase is a work of people as their day job?
In the case of Linux, I think currently all of the most important contributors (who, on the whole, are responsible for almost all of the incoming core code) are now getting paid for their work on Linux (at OSDL, Red Hat, SUSE, IBM etc.). The same is true for Mozilla (Mozilla Foundation, Oracle, IBM, and now, famously, Google). Of course, this wasn't always so. Anyway, what's the case with KDE?
This rebruttal is not working, unfortunately. The maintainers of the random webserver can change the content of the mirror to malicious code.
Famously, if you google for "wares", you will get this spell-checking suggestion from google: "Did you mean: warez ?".
This is the third or fouth time that someone points to faser.net/mab on this thread as an example of a good XUL application. No other examples mentioned at Score:5. That thing is very-very cool indeed. But I'd really like to know why aren't there many more of these.
Please mod parent UP. This is the most insightful remark on time travel I have ever read. And I read a lot. 808140, please recommend some further reading. :)
I really liked your explanation about scientists answering why-questions with how-answers. But let me mention a possible point where science gives a why-answer in this sense. The Anthropic Principle is generally frowned upon, because the answer it gives is unsatisfying and can even be considered nihilistic. But it is a why-answer.
Important quote:
"Customers that do web application development heavily use DHTML and other special features that Konqueror doesn't handle very well and it is a lot of work to implement this. Although I like KHTML and the architecture quite a bit I am sad to say that probably the Gecko rendering engine will be the dominant one used in the enterprise arena, and as KDE developers we've got to make sure that we can integrate Gecko fairly well into KDE.
So Lars Knoll and Zack Rusin started working on this at aKademy and I was delighted when they put me aside and showed me what they have done in just three days. It is amazing! I think it is the right way to go! It is a bit sad for KHTML and I hope that despite this people will still maintain it as it is a nice lightweight browser. If it would be a purely technical decision, KHTML has the better architecture, but sometimes you need to go the shortest way to get to your target."
"I don't want to make 101 decisions when I work on my computer. I want sensible defaults and not have to care about plethoras of unneeded options."
You pick one of 101 options everytime you press a key on your standard 101-key desktop keyboard. I recommend the F1 key as a sensible default.
Why is it just as unlikely? Would there be any interesting consequences if NP=co-NP? It doesn't help resolve the P=NP question.
I'll give two different answers. Neither will be fully convincing.
1. Some of the most interesting mathematical theorems have this form: "The existence of an object and the nonexistence of another object are logically equivalent." Linear algebra and linear programming duality, the Nullstellensatz and the theory of matchings are nice examples of this. NP=co-NP would mean that we automatically get such theorems for any possible NP search question, like the existence of cliques, satisfying assingments and so on.
2. Both P=NP and NP=co-NP are stronger versions of "the polynomial hierarchy collapses" statement. Speaking in metaphors, P=NP says that "every imaginable bounded-round two-player game is easy to play". NP=co-NP says that "every imaginable bounded-round two-player game is as easy as solitaire". The collapse statement says something like "many-round two-player games are no harder than k-round two-player games, for some fixed k." Even this much weaker statement is considered very unlikely by computer scientists.