Your argument doesn't work because nothing is ultimately "verifiable"--there is always a non-zero probability of error. You can't completely verify the proof checker, and you can't completely verify the original proof.
A proof checker, however, greatly lowers the probability of error because it automates a tedious and repetitive task. Furthermore, a proof checker can be tested with test cases, while a human cannot (humans don't work reproducibly).
It's like accounting: you can do it by hand, but you generally get more reliable results from a computer.
Well, you have to verify that your proof checker is correct. Fortunately, that's a much easier problem because proof checkers are much simpler than complex mathematical proofs and because you can test proof checkers over a large number of known proofs to gain confidence in their correctness.
You can attempt proving that your proof checker itself is correct. However, given that everything is at some point created and/or interpreted by humans, you can never have complete certainty. But a proof checker gives you a lot more confidence than a bunch of human experts.
Yes computers can do things faster, but ever underestimate the power of truly knowing what your doing, which so far, a computer can't grasp at all, let alone do as well as the human mind.
Finding a proof may require human imagination; verifying a proof should not. If it does, the proof is incomplete.
But even multiple computers performing a verify isn't _truly_ a verification.
Well, as far as I'm concerned, even multiple mathematicians "performing a verify" isn't truly a verification. Until a proof has been formalized and verified by a well-tested automated proof verifier, it remains an unverified proof sketch.
After all, how long did the Pentium division bug go _unnoticed_???
Well, Intel obviously failed to verify their design, probably because they exhibited the same hubris as you do. However, unlike erroneous mathematical proofs, which just languish unnoticed in mathematical journals for decades or centuries, when hardware companies fail to verify their designs, someone notices because they get wrong results.
What this amounts to is that BitKeeper used Linux as a marketing trick to gain acceptance and recognition for their product, as well as to get bugs out and features for large-scale develoment in, and now that they have gotten what they want, they are dumping their free tool and focusing on making money.
In fact, this sort of behavior isn't uncommon. Open source projects should be careful about letting themselves be used in this way. All the marketing, bug reporting, and feature requests you contribute to a vendor are very valuable; they could be going to an open source project instead.
Think of this in terms of money: if someone gave you a million dollars to spend on a tool, would you contribute it to a commercial company for a three year license for their tool, or would you spend it on an open source project to help develop a free alternative? I think if you really believe that open source is a viable approach to software development, you should choose the latter.
He pointed out that as a long-time open source fanatic and the CEO of BitMover, "we represent as open-source friendly a commercial organization as you are *ever* going to see", cautioning that the events that have caused BitMover to phase out its free product could also result in other companies never even bothering to make products available on Linux.
That's OK--we don't need companies with that kind of business model for commodity applications.
"back at Sun they had a saying 'it's the apps, stupid'.
Yes, and by following Sun's advice, you can run your business into the ground just like Sun is doing. You see, trying to compete against commodity software is stupid. Java-like systems have become a commodity, and so have BitKeeper-like systems. Sun, at least, figured it out for OpenOffice.
Which meant that all the 'my OS is better than your OS' rhetoric was nothing compared to having more applications on your platform than the other guy's platform.
We have enough applications on Linux, thank you very much, including probably a dozen version control systems that are pretty good. One of them (maybe Subversion) will now end up being used for kernel development, and as a result, it will receive enough attention to become truly competitive with BitKeeper.
Linus's decision to use BitKeeper for Linux, unfortunately, prevented that from happening earlier, which condemned a lot of secondary users of open source version control tools to using less mature tools than they otherwise would have. I hope Linus learned a lesson from this as well: eat open source dog food--it may be painful in the short term, but in the long term, it helps the whole community.
If you don't like a license, don't use the software. It's as simple as that.
I don't like Sun's licenses on Java, which is why I don't use their software. It's a simple as that.
And if you value the future of open source software and programming freedom, I recommend you don't use Sun Java either--Sun is dangerous because not only are their licenses proprietary, they are also trying to trick people into thinking that they are open.
Even if you consider constructs like the reals, they are actually quite inelegant. The same can be said for a lot of other mathematical constructs and proofs.
The problem with modern computer aided proofs is they allow the proof to become unwieldy and overly verbose, compared to what it would have to be if just a human produced it.
The problem with a lot of human proofs is that they are wrong and that they are wrong in such subtle ways that human readers don't notice.
If you can't independently examine and verify your "proof" then how can it be considered proof of anything?
By programming my computer to independently examine and verify the proof. Done properly, the instructions for a computer to verify a proof can be a lot simpler than verifying the proof itself.
RTFA. Yes, they do plan on removing their breathing apparatus, like after the reenter the capsule. Dust on the outside of their space suits then gets into the capsule. Article also contains possible solutions. You should read it.
Your a bunch of idiots, a new and better probe is coming, Voyager isn't needed anymore.
The two missions are different, and, besides, any data we get from Voyager helps us better plan future exploration in that area. It is money well spent.
Why do you think we sent such a dinky probe to Titan? It was to get the rough data that then lets us plan for real exploration.
but you pick some programs to cut from that budget
Easy: cancel the ISS, cancel the entire shuttle program, and cancel manned trips to moon and Mars. NASA would then have plenty of money to do real science and to work in peace on better propulsion systems.
Revisit manned space travel in another decade or two, when we have the technology to do a good job at it, developed as part of unmanned space travel and advances in other fields.
Trademarks are there to identify products--both in their good and in their bad aspects. It is completely appropriate to use a trademark to say bad things about a product.
What you cannot do is cybersquat (occupy a trademarked domain name for the purpose of selling it to the trademark holder) or mislead trick people into buying goods under the trademarked name without authorization of the trademark holder.
It's funny, just in reverse. A Voodoo 2 with 6M of RAM is already hugely powerful. People used to do gaming on Apple II's and Commodore 64's, with 64K of memory and no hardware acceleration, even some simple 3D games (Wolfenstein).
I think you'll find that the physics of water molecule resonance had something to do with choice of this band.
Less than one might think. Microwaves over a fairly broad range of frequencies work--more than enough for different countries to choose different frequencies. In fact, I wouldn't be surprised if they have.
If that was all there was to it, then the commission would have already abandoned demands for the ability to create open source software because "available for licensing [...] if you pay the license fee" is incompatible with open source. Since the debate is still on-going, obviously, that can't be all there is to it.
Look for "mini-itx linux preinstalled" on Google; you'll find a bunch of hits.
Yes, it is a bummer that there are no major vendors doing this and marketing it, but Mini-ITX are kind of specialty systems. There are plenty of bigger vendors that sell other Linux systems (including small ones) preinstalled.
"We are working with the Commission to try to find a way that companies can implement these technologies in code that would get distributed with open source products, but the source code wouldn't be published itself so that the confidentiality of our information is preserved," the spokesperson added.
It sounds like Microsoft is not even talking about access to their source code, they are talking about whether open source projects are permitted to distribute their own code necessary for interoperating with Microsoft code in open source form.
In different words, Microsoft is trying to keep "confidential" exactly what the commission is requiring them to make public.
Furthermore, since the only group of people they are trying to impose restrictions on is open source (since binary-only vendors have full access under the agreement already), this is a direct attack by Microsoft on open source.
Well, it's good to see that Microsoft is validating open source through their action. Let's hope that the EU doesn't let them get away with this.
Ah, I see, another member of the Apple-sponsored "JUST WORKS" marketing campaign.
Everything always "JUST WORKS" on machines with preinstalled supported operating systems, whether it's OSX, Windows, or Linux. Things can stop working once you start installing third party apps or new hardware, on any of those systems, including the Mac Mini.
Actually my views have little to do with the bush administration, and pre-date his fathers administration
That's irrelevant--they still coincide with his on global warming.
No I don't have a Doctorate in anything, I would rather work and make a living than pay a University to validate me
OK, so you don't have any degree to make any determination of the validity of the scientific conclusions that, what you call "the global warming lobby", has reached.
And it wasn't for short term business reasons. Quite the opposite.
That amounts to saying that sticking with tried-and-true technologies is the best business strategy for the US; more than a century of experience, both at the corporate and at the national level, has shown that that is false. Companies and nations that stick their head in the sand when new technologies come out invariably fall behind and that is going to happen to the US unless it invests massively in new energy technologies.
"Look all of them believe in it, lets all go jump over the cliff. "
So, you are saying that switching to new, non-fossil fuel-based technologies, reducing dependence on oil, and investing in new infrastructure is "jumping over the cliff"? Come on, just think about that for a moment: you characterize the adoption of new, efficient technologies as suicide and would rather stick with the tried and true. Obviously, you are the "lemming" and "luddite", not I.
Your nutty statements about global warming coincide pretty much with the Bush party line. In the US political spectrum, you are right wing--sorry if that label makes you uncomfortable.
I prefer to research the data and come to my own conclusions,
Do you have a Ph.D. in physics, mathematics, biology, chemistry, or climatology? Have you published anything peer reviewed on global warming? If not, why should anybody give a fck what you think about the data?
but your perfectly happy to let activists pull your strings and tell you what to say.
"Left activists" like the governments that signed on to the Kyoto treaty, based on input from thousands of national scientific advisors all over the world?
Stop deluding yourself: when dozens of nations are willing to commit billions of dollars towards reducing carbon emissions, that IS the mainstream view. The US is the sad exception because its politics have been hijacked by short-term corporate interests.
If you want a doom and gloom scenario, following religous type luddites such as yourself who's only motivation is political and anti-business is the sure path to destruction.
You got it backwards. It's people like you who are luddites, anti-technology, and anti-business. You want to condemn us unnecessarily to a heavily subsidized, inefficient, technologically outdated oil-based infrastructure. Instead of new investments and business activity resulting from an overhaul of our transportation and energy infrastructure, you want a few existing big players to simply sit on their outdated technologies and continue to reap profits from them. Your faith in technology is so pathetically limited that you don't even believe that technology is capable of delivering cars that don't consume large amounts of fossil fuels and spew out pollutants.
In fact, I have far more faith in technology than you do. I know technology is capable, today, of delivering cars that have a tiny fraction of the amount of impact on the environment than the subsidized, inefficient behemoths that are our only choices today. I know what a shot in the arm for businesses and the economy it would be if hundreds of millions of inefficient gas guzzlers were replaced with new, high-tech vehicles; if we replaced outdated and inefficient homes, factories, and street lighting with modern and efficient versions.
Even if the dangers of CO2 emissions weren't such a well-established fact, moving to these new technologies would make sense for a whole host of other reasons, including the local damage to the environment from current vehicles, the environmental costs of oil, and the political costs of reliance on fossil fuels.
The anti-business luddite is people like you, statists who have no faith in new technologies and who think that any change or cooperation is a threat to their security.
Luckily your invective rhetoric is sperating yourself from the regular populace.
You right wing nuts cowed the whole nation into being a bunch of scared little sissies with your invective rhetoric, afraid of change, afraid of new technology, afraid of terrorism, and afraid of the rest of the world. Instead of facing problems, you prefer to stick your head in the sand and pray, and when you get really scared that something might change, you confuse the nation with non-issues like "gay marriage" and "right to life".
Of course, you personally are just a puppet whose strings are being pulled. But it's time one took the initiative back from the people who manipulate people like you for their own self interest. And if it takes "invective rhetoric" to fight "invective rhetoric", so be it.
Well it's obvious you've bought into the religion hook line and sinker.
Why shouldn't I? It's the scientific mainstream, and it's the basis of an international treaty to which dozens of nations have committed billions of dollars.
Your position, on the other hand, is not only a fringe position in the scientific community, its adoption by a tiny minority is fully explicable by short-term economic and political self-interest, with a callous disregard for the long term safety and well-being of others.
And I like how you keep calling me wrong and ill-informed without actually putting forth any facts to refute the facts and citatations I've put forward.
You know, some positions are just so ludicrous and so far removed from the scientific mainstream that it's not worth debating them point by point. Creationists, flat earthers, and people like you simply don't warrant a point-by-point rebuttal anymore--you are inaccessible to rational debate anyway, and all the facts are out there in abundance.
This is useful research, but it's incremental and verges on engineering. Gestural interaction for both mobile devices and stationary computers is well studied, as is 3D audio.
Most likely, in the real world, you'll end up with Bluetooth headsets and acceleration sensors in your devices for simple gestural interactions: cheap, reliable technologies.
Slashdot Mirror
Your argument doesn't work because nothing is ultimately "verifiable"--there is always a non-zero probability of error. You can't completely verify the proof checker, and you can't completely verify the original proof.
A proof checker, however, greatly lowers the probability of error because it automates a tedious and repetitive task. Furthermore, a proof checker can be tested with test cases, while a human cannot (humans don't work reproducibly).
It's like accounting: you can do it by hand, but you generally get more reliable results from a computer.
Well, you have to verify that your proof checker is correct. Fortunately, that's a much easier problem because proof checkers are much simpler than complex mathematical proofs and because you can test proof checkers over a large number of known proofs to gain confidence in their correctness.
You can attempt proving that your proof checker itself is correct. However, given that everything is at some point created and/or interpreted by humans, you can never have complete certainty. But a proof checker gives you a lot more confidence than a bunch of human experts.
Yes computers can do things faster, but ever underestimate the power of truly knowing what your doing, which so far, a computer can't grasp at all, let alone do as well as the human mind.
Finding a proof may require human imagination; verifying a proof should not. If it does, the proof is incomplete.
But even multiple computers performing a verify isn't _truly_ a verification.
Well, as far as I'm concerned, even multiple mathematicians "performing a verify" isn't truly a verification. Until a proof has been formalized and verified by a well-tested automated proof verifier, it remains an unverified proof sketch.
After all, how long did the Pentium division bug go _unnoticed_???
Well, Intel obviously failed to verify their design, probably because they exhibited the same hubris as you do. However, unlike erroneous mathematical proofs, which just languish unnoticed in mathematical journals for decades or centuries, when hardware companies fail to verify their designs, someone notices because they get wrong results.
What this amounts to is that BitKeeper used Linux as a marketing trick to gain acceptance and recognition for their product, as well as to get bugs out and features for large-scale develoment in, and now that they have gotten what they want, they are dumping their free tool and focusing on making money.
In fact, this sort of behavior isn't uncommon. Open source projects should be careful about letting themselves be used in this way. All the marketing, bug reporting, and feature requests you contribute to a vendor are very valuable; they could be going to an open source project instead.
Think of this in terms of money: if someone gave you a million dollars to spend on a tool, would you contribute it to a commercial company for a three year license for their tool, or would you spend it on an open source project to help develop a free alternative? I think if you really believe that open source is a viable approach to software development, you should choose the latter.
He pointed out that as a long-time open source fanatic and the CEO of BitMover, "we represent as open-source friendly a commercial organization as you are *ever* going to see", cautioning that the events that have caused BitMover to phase out its free product could also result in other companies never even bothering to make products available on Linux.
That's OK--we don't need companies with that kind of business model for commodity applications.
"back at Sun they had a saying 'it's the apps, stupid'.
Yes, and by following Sun's advice, you can run your business into the ground just like Sun is doing. You see, trying to compete against commodity software is stupid. Java-like systems have become a commodity, and so have BitKeeper-like systems. Sun, at least, figured it out for OpenOffice.
Which meant that all the 'my OS is better than your OS' rhetoric was nothing compared to having more applications on your platform than the other guy's platform.
We have enough applications on Linux, thank you very much, including probably a dozen version control systems that are pretty good. One of them (maybe Subversion) will now end up being used for kernel development, and as a result, it will receive enough attention to become truly competitive with BitKeeper.
Linus's decision to use BitKeeper for Linux, unfortunately, prevented that from happening earlier, which condemned a lot of secondary users of open source version control tools to using less mature tools than they otherwise would have. I hope Linus learned a lesson from this as well: eat open source dog food--it may be painful in the short term, but in the long term, it helps the whole community.
If you don't like a license, don't use the software. It's as simple as that.
I don't like Sun's licenses on Java, which is why I don't use their software. It's a simple as that.
And if you value the future of open source software and programming freedom, I recommend you don't use Sun Java either--Sun is dangerous because not only are their licenses proprietary, they are also trying to trick people into thinking that they are open.
Are you trying to be subtly funny here? Computers can routinely beat human chess players, even the best of them.
The best math is always elegant.
Even if you consider constructs like the reals, they are actually quite inelegant. The same can be said for a lot of other mathematical constructs and proofs.
The problem with modern computer aided proofs is they allow the proof to become unwieldy and overly verbose, compared to what it would have to be if just a human produced it.
The problem with a lot of human proofs is that they are wrong and that they are wrong in such subtle ways that human readers don't notice.
If you can't independently examine and verify your "proof" then how can it be considered proof of anything?
By programming my computer to independently examine and verify the proof. Done properly, the instructions for a computer to verify a proof can be a lot simpler than verifying the proof itself.
RTFA. Yes, they do plan on removing their breathing apparatus, like after the reenter the capsule. Dust on the outside of their space suits then gets into the capsule. Article also contains possible solutions. You should read it.
Your a bunch of idiots, a new and better probe is coming, Voyager isn't needed anymore.
The two missions are different, and, besides, any data we get from Voyager helps us better plan future exploration in that area. It is money well spent.
Why do you think we sent such a dinky probe to Titan? It was to get the rough data that then lets us plan for real exploration.
but you pick some programs to cut from that budget
Easy: cancel the ISS, cancel the entire shuttle program, and cancel manned trips to moon and Mars. NASA would then have plenty of money to do real science and to work in peace on better propulsion systems.
Revisit manned space travel in another decade or two, when we have the technology to do a good job at it, developed as part of unmanned space travel and advances in other fields.
Trademarks are there to identify products--both in their good and in their bad aspects. It is completely appropriate to use a trademark to say bad things about a product.
What you cannot do is cybersquat (occupy a trademarked domain name for the purpose of selling it to the trademark holder) or mislead trick people into buying goods under the trademarked name without authorization of the trademark holder.
It's funny, just in reverse. A Voodoo 2 with 6M of RAM is already hugely powerful. People used to do gaming on Apple II's and Commodore 64's, with 64K of memory and no hardware acceleration, even some simple 3D games (Wolfenstein).
I think you'll find that the physics of water molecule resonance had something to do with choice of this band.
Less than one might think. Microwaves over a fairly broad range of frequencies work--more than enough for different countries to choose different frequencies. In fact, I wouldn't be surprised if they have.
If that was all there was to it, then the commission would have already abandoned demands for the ability to create open source software because "available for licensing [...] if you pay the license fee" is incompatible with open source. Since the debate is still on-going, obviously, that can't be all there is to it.
Look for "mini-itx linux preinstalled" on Google; you'll find a bunch of hits.
Yes, it is a bummer that there are no major vendors doing this and marketing it, but Mini-ITX are kind of specialty systems. There are plenty of bigger vendors that sell other Linux systems (including small ones) preinstalled.
"We are working with the Commission to try to find a way that companies can implement these technologies in code that would get distributed with open source products, but the source code wouldn't be published itself so that the confidentiality of our information is preserved," the spokesperson added.
It sounds like Microsoft is not even talking about access to their source code, they are talking about whether open source projects are permitted to distribute their own code necessary for interoperating with Microsoft code in open source form.
In different words, Microsoft is trying to keep "confidential" exactly what the commission is requiring them to make public.
Furthermore, since the only group of people they are trying to impose restrictions on is open source (since binary-only vendors have full access under the agreement already), this is a direct attack by Microsoft on open source.
Well, it's good to see that Microsoft is validating open source through their action. Let's hope that the EU doesn't let them get away with this.
everything on the Mac Mini JUST WORKS.
Ah, I see, another member of the Apple-sponsored "JUST WORKS" marketing campaign.
Everything always "JUST WORKS" on machines with preinstalled supported operating systems, whether it's OSX, Windows, or Linux. Things can stop working once you start installing third party apps or new hardware, on any of those systems, including the Mac Mini.
Tiny fans actually tend to be noiser.
In any case, another reason not to use fans is that they fail frequently, lowering overall reliability.
Actually my views have little to do with the bush administration, and pre-date his fathers administration
That's irrelevant--they still coincide with his on global warming.
No I don't have a Doctorate in anything, I would rather work and make a living than pay a University to validate me
OK, so you don't have any degree to make any determination of the validity of the scientific conclusions that, what you call "the global warming lobby", has reached.
And it wasn't for short term business reasons. Quite the opposite.
That amounts to saying that sticking with tried-and-true technologies is the best business strategy for the US; more than a century of experience, both at the corporate and at the national level, has shown that that is false. Companies and nations that stick their head in the sand when new technologies come out invariably fall behind and that is going to happen to the US unless it invests massively in new energy technologies.
"Look all of them believe in it, lets all go jump over the cliff. "
So, you are saying that switching to new, non-fossil fuel-based technologies, reducing dependence on oil, and investing in new infrastructure is "jumping over the cliff"? Come on, just think about that for a moment: you characterize the adoption of new, efficient technologies as suicide and would rather stick with the tried and true. Obviously, you are the "lemming" and "luddite", not I.
Attacking my "Right Wing" beliefs.
Your nutty statements about global warming coincide pretty much with the Bush party line. In the US political spectrum, you are right wing--sorry if that label makes you uncomfortable.
I prefer to research the data and come to my own conclusions,
Do you have a Ph.D. in physics, mathematics, biology, chemistry, or climatology? Have you published anything peer reviewed on global warming? If not, why should anybody give a fck what you think about the data?
but your perfectly happy to let activists pull your strings and tell you what to say.
"Left activists" like the governments that signed on to the Kyoto treaty, based on input from thousands of national scientific advisors all over the world?
Stop deluding yourself: when dozens of nations are willing to commit billions of dollars towards reducing carbon emissions, that IS the mainstream view. The US is the sad exception because its politics have been hijacked by short-term corporate interests.
If you want a doom and gloom scenario, following religous type luddites such as yourself who's only motivation is political and anti-business is the sure path to destruction.
You got it backwards. It's people like you who are luddites, anti-technology, and anti-business. You want to condemn us unnecessarily to a heavily subsidized, inefficient, technologically outdated oil-based infrastructure. Instead of new investments and business activity resulting from an overhaul of our transportation and energy infrastructure, you want a few existing big players to simply sit on their outdated technologies and continue to reap profits from them. Your faith in technology is so pathetically limited that you don't even believe that technology is capable of delivering cars that don't consume large amounts of fossil fuels and spew out pollutants.
In fact, I have far more faith in technology than you do. I know technology is capable, today, of delivering cars that have a tiny fraction of the amount of impact on the environment than the subsidized, inefficient behemoths that are our only choices today. I know what a shot in the arm for businesses and the economy it would be if hundreds of millions of inefficient gas guzzlers were replaced with new, high-tech vehicles; if we replaced outdated and inefficient homes, factories, and street lighting with modern and efficient versions.
Even if the dangers of CO2 emissions weren't such a well-established fact, moving to these new technologies would make sense for a whole host of other reasons, including the local damage to the environment from current vehicles, the environmental costs of oil, and the political costs of reliance on fossil fuels.
The anti-business luddite is people like you, statists who have no faith in new technologies and who think that any change or cooperation is a threat to their security.
Luckily your invective rhetoric is sperating yourself from the regular populace.
You right wing nuts cowed the whole nation into being a bunch of scared little sissies with your invective rhetoric, afraid of change, afraid of new technology, afraid of terrorism, and afraid of the rest of the world. Instead of facing problems, you prefer to stick your head in the sand and pray, and when you get really scared that something might change, you confuse the nation with non-issues like "gay marriage" and "right to life".
Of course, you personally are just a puppet whose strings are being pulled. But it's time one took the initiative back from the people who manipulate people like you for their own self interest. And if it takes "invective rhetoric" to fight "invective rhetoric", so be it.
Well it's obvious you've bought into the religion hook line and sinker.
Why shouldn't I? It's the scientific mainstream, and it's the basis of an international treaty to which dozens of nations have committed billions of dollars.
Your position, on the other hand, is not only a fringe position in the scientific community, its adoption by a tiny minority is fully explicable by short-term economic and political self-interest, with a callous disregard for the long term safety and well-being of others.
And I like how you keep calling me wrong and ill-informed without actually putting forth any facts to refute the facts and citatations I've put forward.
You know, some positions are just so ludicrous and so far removed from the scientific mainstream that it's not worth debating them point by point. Creationists, flat earthers, and people like you simply don't warrant a point-by-point rebuttal anymore--you are inaccessible to rational debate anyway, and all the facts are out there in abundance.
This is useful research, but it's incremental and verges on engineering. Gestural interaction for both mobile devices and stationary computers is well studied, as is 3D audio.
Most likely, in the real world, you'll end up with Bluetooth headsets and acceleration sensors in your devices for simple gestural interactions: cheap, reliable technologies.