It's worth noting that Sun's Fortress project was not selected for Phase III of DARPA's HPCS project. (And for good measure, a link to a blog at Sun and an FAQ on how Fortress relates to the other HPCS languages/projects.)
On a related note to the article, it's worth pointing out that the POPLmark Challenge aims to bring computer-verified and computer-aided proof to a wider audience, in this case programming language researchers. The challenge programs are chosen to exercise many aspects of programming languages that are known to be difficult to formalize.
The site has much more information about our particular motivations, but the basic idea is many proofs about programming languages are long, tedious, and otherwise uninteresting. However, one (small) mistake can invalidate large amounts of work, and there are indeed examples of this in the literature. We hope that theorem proving technology can help us avoid these pitfalls, but it appears that for the moment, the technology needs to improve a bit.
This is kind of a side remark that I haven't really thought on too much, but here goes. (I think I'm playing devil's advocate...)
(1) Who audits the open source software that they use? I certainly don't. I rarely even bother to look at the source. So in this respect, it doesn't matter (to me) if the software is closed source or open source since the code isn't looked at even if you (I) had the chance to.
(2) If you're not going to audit the code, will you trust the code developers to have done adequate auditing? Again, the folks who write open source software are, for the most part, as much a stranger as the folks working in some company (at least if you're me). Why should I trust "open source" strangers more than "closed source" strangers?
These points rarely seem to get brought up here. I can certainly see the answers to (2) giving the edge to open source, but what about (1)?.
Hate to break it to you, but by buying the songs, you (or whoever bought them) agreed to the following restrictions (which I cut and paste from the iTunes Music Store Terms of Service).
b. Use of Products. You acknowledge that Products contain security technology that limits your usage of Products to the following Usage Rules, and you agree to use Products in compliance with such Usage Rules.
Usage Rules.
Your use of the Products is conditioned upon your prior acceptance of the terms of this Agreement.
You shall be authorized to use the Products only for personal, noncommercial use.
You shall be authorized to use the Products on three Apple-authorized computers at any time.
You shall be entitled to export, burn or copy Products solely for personal, noncommercial use.
Any burning or exporting capabilities are solely an accommodation to you and shall not constitute a grant or waiver (or other limitation or implication) of any rights of the copyright owners in any content, sound recording, underlying musical composition, or artwork embodied in any Product.
You agree that you will not attempt to, or encourage or assist any other person to, circumvent or modify any security technology or software that is part of the Service or used to administer the Usage Rules.
The delivery of Products does not transfer to you any commercial or promotional use rights in the Products.
The problem with computer generated proofs is that in order to trust the result of the computer, you have to trust:
The program(s), as source code, that generated the proofs.
The compiler(s) that turned the source code into something executable.
The hardware that ran the programs.
And of course, our understanding of the hardware depends on how accurate our understanding of the laws of physics is. Any mistake in either the source code, compiler, or hardware, and potentially the proof produced is incorrect. That's an awful amount of stuff you have to check just to make absolutely sure the computer is correct. Then, consider how many bug-free pieces of software you've encountered.... Yeah, I can see why mathematicians would not trust computer generated proofs.
Of course, people are not infallible either, but that's well known and expected. It's all about how much uncertainty people are willing to accept.
Re:The whole streaming audio/video field's gone cr
on
Real Problems
·
· Score: 1
Care to provide some justification as to exactly how Mac OS X and the Quicktime player software are spyware-riddled and or bloatware? (Being a Mac user, I'm curious to hear about this.) Besides, as far as Quicktime goes, it's an open container format. The codecs used to encode/decode the streams are an entirely separate issue.
Another thing to consider: why is your machine thrashing? If what you're working with can't fit in RAM, then that's likely your real problem, not how efficiently you implement a swap file/partition. Compared to RAM, hard drive access is glacially slow, regardless of how you set things up.
Most operating systems today should be able to deal with swap files/partitions with reasonable performance, without you having to go to great lengths to optimize things. So probably the "default setup" (whatever that may be) will be fine, unless you really need that last ounce of performance.
I found its offerings to be professional and compentent, if unremarkable. So far the site seems to deliver on what its promising. FREE downloads, FREE streaming audio. Their business model appears to be ethical (by my standards).
Basically I'm waiting a week or two to see in the media if things are kosher before buying something: e.g. this is a legitimate venture?; they're on the up & up?; people don't have nasty customer service problems, etc.
I've bought one CD from them after listening to the entire thing first a few times (in case your curious, it was "Shall We Dance" by Beth Quist). Other than the fact that it seemed that you had to use PayPal to pay for your purchase, the service was quite good. Once they received the payment, I was emailed with instructions on how I could download WAV and MP3 versions of the CD. No restrictions on the files, and the download process was straightforward.
The fact that you could also name your price (from $5 to $18 in $1 increments) was also really cool. Hopefully, they'll keep this method of payment (it is something that they were trying out to see how well it would work). Most people seem to pay about $8 (the amount they recommend). And the artist gets half of whatever you pay, which I think is much better than your typical CD (at least from what I've heard).
If all these performance hacks are documented, why doesn't the compiler implement them?
The most common reason is that most performance hacks and optimizations are not decidable, and you want a compiler to implement only decidable algorithms becuase those are the ones that enable a compiler to be deterministic. It is usually much easier for a person, i.e., human, to determine what can be done, than it is for a machine to determine that exact same thing.
Consider the following piece of code.
boolean f(int[] a, int[] b)
{
int x = a[0];
b[0] = a[0] + 2;
int y = a[0];
return (x == y);
}
Does f always return true? Only if we can prove that a and b never point to the same array. A person maybe able to do this, but a machine would have great difficulty (assuming the machine could even do it).
So to sumarize, compiler's don't implement many optimization hacks becuase then they might not be deterministic, and that is a bad thing.
csh/tcsh...well, google for "csh Programming Considered Harmful" to see its many internal bugs. Also, most of the major Unices don't use it (Solaris, AIX, Linux - I guess *BSD might still) for their system stuff. If it's not considered a good scripting platform AND most Unices don't use it for their scripts...
No one said the shell you use has to be the one you program in.
I prefer to use tcsh for my interactive shell (it does everything that I need it to), but use sh for shell scripting (since it's on every platform I work on).
Re:Physics has always been ethically compromised
on
Ununoctium Wrapup
·
· Score: 1
Milliken guessed or decided beforehand what he wanted the electrostatic constant to be and kept fudging his results until he got the one he wanted.
This is an unduly harsh analysis of Millikan's result and publication. There is no evidence to indicate that Millikan had guessed what he wanted, and then chose to the data to fit that.
I suggest that you check out an article in The American Scientist (available freely in a
posting
by David Goodstein (Caltech)).
To briefly summarize that American Scientist article, Millikan had very exacting standards for the data that he would publish. If the oil drops were too small, too much effected by Brownian motion, or affected by innaccuracy in Stoke's Law (which he documented completely), the results were not published. If the drops fell to quickly for accurate measurement, the results were not published.
So a marking like "error high, will not use" probably meant that he could not be certain of the numbers that he recorded.
Likewise, even drops that were labeled "the best one I ever had" were not published. Even if the results of all his observations were taken into account, and not just the observations he published, his end result would have not changed significantly.
In short, to say that Millikan "guessed the answer" is at the very least unfair. He chose data that he was confidant had been recorded in a reliable fashion. You might fault him for other things, but not for choosing an answer before hand and then picking experimental results to support that.
Slashdot Mirror
It's worth noting that Sun's Fortress project was not selected for Phase III of DARPA's HPCS project. (And for good measure, a link to a blog at Sun and an FAQ on how Fortress relates to the other HPCS languages/projects.)
On a related note to the article, it's worth pointing out that the POPLmark Challenge aims to bring computer-verified and computer-aided proof to a wider audience, in this case programming language researchers. The challenge programs are chosen to exercise many aspects of programming languages that are known to be difficult to formalize.
The site has much more information about our particular motivations, but the basic idea is many proofs about programming languages are long, tedious, and otherwise uninteresting. However, one (small) mistake can invalidate large amounts of work, and there are indeed examples of this in the literature. We hope that theorem proving technology can help us avoid these pitfalls, but it appears that for the moment, the technology needs to improve a bit.
Check out the ACLU's page on the challenge. There's info on the (redacted) complaint itself, a press release, and related cases and efforts.
Check out Hypertext Help with LaTeX if you need a quick, online reference. Not so great if you actually need to learn LaTeX from scratch, however.
This is kind of a side remark that I haven't really thought on too much, but here goes. (I think I'm playing devil's advocate...)
(1) Who audits the open source software that they use? I certainly don't. I rarely even bother to look at the source. So in this respect, it doesn't matter (to me) if the software is closed source or open source since the code isn't looked at even if you (I) had the chance to.
(2) If you're not going to audit the code, will you trust the code developers to have done adequate auditing? Again, the folks who write open source software are, for the most part, as much a stranger as the folks working in some company (at least if you're me). Why should I trust "open source" strangers more than "closed source" strangers?
These points rarely seem to get brought up here. I can certainly see the answers to (2) giving the edge to open source, but what about (1)?.
Hate to break it to you, but by buying the songs, you (or whoever bought them) agreed to the following restrictions (which I cut and paste from the iTunes Music Store Terms of Service).
b. Use of Products. You acknowledge that Products contain security technology that limits your usage of Products to the following Usage Rules, and you agree to use Products in compliance with such Usage Rules.
Usage Rules.
Your use of the Products is conditioned upon your prior acceptance of the terms of this Agreement.
You shall be authorized to use the Products only for personal, noncommercial use.
You shall be authorized to use the Products on three Apple-authorized computers at any time.
You shall be entitled to export, burn or copy Products solely for personal, noncommercial use.
Any burning or exporting capabilities are solely an accommodation to you and shall not constitute a grant or waiver (or other limitation or implication) of any rights of the copyright owners in any content, sound recording, underlying musical composition, or artwork embodied in any Product.
You agree that you will not attempt to, or encourage or assist any other person to, circumvent or modify any security technology or software that is part of the Service or used to administer the Usage Rules.
The delivery of Products does not transfer to you any commercial or promotional use rights in the Products.
The problem with computer generated proofs is that in order to trust the result of the computer, you have to trust:
And of course, our understanding of the hardware depends on how accurate our understanding of the laws of physics is. Any mistake in either the source code, compiler, or hardware, and potentially the proof produced is incorrect. That's an awful amount of stuff you have to check just to make absolutely sure the computer is correct. Then, consider how many bug-free pieces of software you've encountered. ... Yeah, I can see why mathematicians would not trust computer generated proofs.
Of course, people are not infallible either, but that's well known and expected. It's all about how much uncertainty people are willing to accept.
Care to provide some justification as to exactly how Mac OS X and the Quicktime player software are spyware-riddled and or bloatware? (Being a Mac user, I'm curious to hear about this.) Besides, as far as Quicktime goes, it's an open container format. The codecs used to encode/decode the streams are an entirely separate issue.
Another thing to consider: why is your machine thrashing? If what you're working with can't fit in RAM, then that's likely your real problem, not how efficiently you implement a swap file/partition. Compared to RAM, hard drive access is glacially slow, regardless of how you set things up.
Most operating systems today should be able to deal with swap files/partitions with reasonable performance, without you having to go to great lengths to optimize things. So probably the "default setup" (whatever that may be) will be fine, unless you really need that last ounce of performance.
I found its offerings to be professional and compentent, if unremarkable. So far the site seems to deliver on what its promising. FREE downloads, FREE streaming audio. Their business model appears to be ethical (by my standards).
Basically I'm waiting a week or two to see in the media if things are kosher before buying something: e.g. this is a legitimate venture?; they're on the up & up?; people don't have nasty customer service problems, etc.
I've bought one CD from them after listening to the entire thing first a few times (in case your curious, it was "Shall We Dance" by Beth Quist). Other than the fact that it seemed that you had to use PayPal to pay for your purchase, the service was quite good. Once they received the payment, I was emailed with instructions on how I could download WAV and MP3 versions of the CD. No restrictions on the files, and the download process was straightforward.
The fact that you could also name your price (from $5 to $18 in $1 increments) was also really cool. Hopefully, they'll keep this method of payment (it is something that they were trying out to see how well it would work). Most people seem to pay about $8 (the amount they recommend). And the artist gets half of whatever you pay, which I think is much better than your typical CD (at least from what I've heard).
If all these performance hacks are documented, why doesn't the compiler implement them?
The most common reason is that most performance hacks and optimizations are not decidable, and you want a compiler to implement only decidable algorithms becuase those are the ones that enable a compiler to be deterministic. It is usually much easier for a person, i.e., human, to determine what can be done, than it is for a machine to determine that exact same thing.
Consider the following piece of code.
boolean f(int[] a, int[] b)
{
int x = a[0];
b[0] = a[0] + 2;
int y = a[0];
return (x == y);
}
Does f always return true? Only if we can prove that a and b never point to the same array. A person maybe able to do this, but a machine would have great difficulty (assuming the machine could even do it).
So to sumarize, compiler's don't implement many optimization hacks becuase then they might not be deterministic, and that is a bad thing.
csh/tcsh...well, google for "csh Programming Considered Harmful" to see its many internal bugs. Also, most of the major Unices don't use it (Solaris, AIX, Linux - I guess *BSD might still) for their system stuff. If it's not considered a good scripting platform AND most Unices don't use it for their scripts...
No one said the shell you use has to be the one you program in. I prefer to use tcsh for my interactive shell (it does everything that I need it to), but use sh for shell scripting (since it's on every platform I work on).
This is an unduly harsh analysis of Millikan's result and publication. There is no evidence to indicate that Millikan had guessed what he wanted, and then chose to the data to fit that. I suggest that you check out an article in The American Scientist (available freely in a posting by David Goodstein (Caltech)).
To briefly summarize that American Scientist article, Millikan had very exacting standards for the data that he would publish. If the oil drops were too small, too much effected by Brownian motion, or affected by innaccuracy in Stoke's Law (which he documented completely), the results were not published. If the drops fell to quickly for accurate measurement, the results were not published. So a marking like "error high, will not use" probably meant that he could not be certain of the numbers that he recorded. Likewise, even drops that were labeled "the best one I ever had" were not published. Even if the results of all his observations were taken into account, and not just the observations he published, his end result would have not changed significantly.
In short, to say that Millikan "guessed the answer" is at the very least unfair. He chose data that he was confidant had been recorded in a reliable fashion. You might fault him for other things, but not for choosing an answer before hand and then picking experimental results to support that.