> Can anyone comment on why memory usage was selected?
Wild guess: maybe because the hardware it runs on only has 128MB of RAM and no swap space? Without any indication of memory consumption you'd suddenly be unable to launch new apps (erhhh, sorry, activities;-) ) without any apparent reason.
In general, it is impossible to prove that such a 'formal logic validator' is correct since it is not possible to prove that an axiom system is correct inside that axiom system (one of Goedel's theorems). So if you would find a proof that your validator is correct, you'd have used reasoning techniques outside the logic of your validator, and do you believe those? (If so, why didn't you include them in the validator, since now your validator clearly does not support a reasoning technique you considered valid in the first place!)
Basically, at a certain point, you just have to "believe" that your axioms, logic, whatever you call it, is consistent. Because to prove it, you'd again need axioms, a logic, etcetera, ad infinitum.
That's why we talk about "formal mathematical proofs" as opposed to "mathematical proofs". The latter are more or less vague arguments to convince the human reader that a formal mathematical proof of the theorem in question would be possible.
In your proof above, the "mechanically verifiable string manipulations" would amongst others contain substitution (so from the theorem "a+s(b) = s(a+b)" you would be able to get get "s(1)+s(s(1)) = s(s(1)+s(1))" and so on. But it is an informal proof, not a formal one, so to get to the mechanically verifiable level, you'd have to spell out a lot more details.
Yes but a "correct mathematical proof" only establishes truth relative to the axiom system used. Because how will you ever prove that the axioms are true? (That's why they're called axioms---you cannot prove them and just have to assume the're "true".) In other words, there's no such thing as "absolute truth". (This is what Hilbert meant when he defined mathematics as "Mathematics is that subject in which we do not know what we are talking about, nor whether what we say is true.")
Then you'd better check your facts... there must be dozens (if not hundreds---erhhh, speaking about checking ones facts:-) ) of systems in which mathematical theorems are routinely proved (HOL, PVS, Coq, Mizar to name just a few)!
And what if you go up to someone and say "statement blah because here's a (very large) proof that my expert system generated, but which can be verified with a simple program which is just a few pages long"? Remember that *finding* a proof is hard (and hence requires human creativity / AI stuff) but *checking* that a proof is correct is easy (just a bit tedious when the proof is very large, and whom better to trust to do this job than a computer)?
# rpm -Uvh red-carpet-0.9-0_helix_1.i386.rpm
only packages with major numbers <= 3 are supported by this version of RPM
error: red-carpet-0.9-0_helix_1.i386.rpm cannot be installed
Fantastic.
Maybe some day, I'll work out how to update my system enough in order to get this updater. *Sigh*
Re:Open Source does not always require redistribut
on
Open Source And Spying
·
· Score: 1
My version of the GPL says:
You must cause any work that you distribute or publish, that in
whole or in part contains or is derived from the Program or any
part thereof, to be licensed as a whole at no charge to all third
parties under the terms of this License.
So in whatever way they modify, they have to license those modifications as GPL, and as far as I can work out, that means the source of those modifications must be distributed too...
But then again, I an't no lawyer:-)
ReiserFS *is* on the Mandrake CD. I installed my box (mandrake 7.1) without any ext2 partitions whatsoever, everything runs straight off reiserfs partitions.
There is a TeX plugin from IBM, it's called TexExplorer or something like that.
By the way, I don't see how you can do a search in a bunch of text files for a particular kind of formula (``search for all the formulas containing 'something' to the power three inside an integral'')... I hope this MathML stuff will make that kind of things possible.
Hm... i don't agree completely. I skimmed the specs and there are also traditional (risc? don't remember exactly) cpu cores in the chip, so the bulk of the program can be coded the traditional way and only for the time critical part you use the special stuff...
because it creates a situation
in which an IT staffer may make changes that no
one else knows about, and that probably go
undocumented
Every real programmer knows that the source is the documentation!
Seriously though, I don't really see the difference. If you make an undocumented change that is so drastic that everything crashes, documenting it doesn't really seem the remedy to me. Especially if you have a document-every-sneeze policy running, I don't see the advantage of having to search x Mb of docs about x/10 Mb of source code:-)
And the real lesson to be learnt here is that there are a lot of people out there who don't know better... just give them their NT, give them their document-all policy, if they're happy with that, you probably don't want to bother to argue with them anyway:-)
> A program design that fails results in a few hours Me disagreeink. Like that bug in the mars explorer stuff where the one team used inches and the other centimeters... that was *not* noticed after a few hours of programming methinks:-) So formal stuff could be of use also for software. Still don't know really what kind of formal stuff is to be used though (you can go pretty far in that direction).
However, it's interesting to note that when asked where he got all those wonderful names from, Asimov said he simply took usual names and twisted them a bit, and gave the example of Harry ->Hari... if you like trivia;-)
I don't know that much about physics, but the very last paragraph does seem the oddest of all: the mass of the spaceship is always zero, ergo the thing can reach superluminal speeds. Oh nice, at the very beginning, he says that the mass of a photon is always zero. So photons can reach superluminal speeds also, I suppose? Also, I'd like to see how big the radius r_s of that sphere turns out to be in practice... heh:-)
When the iridium satellite passes the field of view of the telescope, you see suddenly a very bright flash because the sattelite is rather reflective... hence the name Iridium Flash:-)
Here at the university of Ghent, Belgium, there's a course in Operating Systems that involves doing stuff with CDROM-device drivers, a parallel port LED driver device, etc... it's at http://www.elis.rug.ac.be/~kdb/best/ but presumably unfortunately most of it is in Dutch:-S
OK, but why is it that whenever a company gives away something for free they have to throw the buzz word 'Open Source' in somewhere? Giving away a compiler for free (as in 'beer') is of course something to be hurrayed upon, but the fact that their press release stuff has to throw in 'Open Source' is misleading, at least. So I'd say, let's pull out the beer, but not the champaign:-)
Maybe the patents are needed in some way to compensate for research costs, but I'd think that nowadays the life-time of patents is much too long. 25 years (or whatever) was maybe fine 100 years ago but nowadays technology of 10 years ago is obsolete, so I'd say that if patents are really a necessary evil (I don't like them anyway), the duration for computer-related patents should be shortened (5 years should be more than long enough to give the google guys their cash). Methinks.
Slashdot Mirror
> Can anyone comment on why memory usage was selected?
;-) ) without any apparent reason.
Wild guess: maybe because the hardware it runs on only has 128MB of RAM and no swap space? Without any indication of memory consumption you'd suddenly be unable to launch new apps (erhhh, sorry, activities
In general, it is impossible to prove that such a 'formal logic validator' is correct since it is not possible to prove that an axiom system is correct inside that axiom system (one of Goedel's theorems). So if you would find a proof that your validator is correct, you'd have used reasoning techniques outside the logic of your validator, and do you believe those? (If so, why didn't you include them in the validator, since now your validator clearly does not support a reasoning technique you considered valid in the first place!)
Basically, at a certain point, you just have to "believe" that your axioms, logic, whatever you call it, is consistent. Because to prove it, you'd again need axioms, a logic, etcetera, ad infinitum.
That's why we talk about "formal mathematical proofs" as opposed to "mathematical proofs". The latter are more or less vague arguments to convince the human reader that a formal mathematical proof of the theorem in question would be possible.
In your proof above, the "mechanically verifiable string manipulations" would amongst others contain substitution (so from the theorem "a+s(b) = s(a+b)" you would be able to get get "s(1)+s(s(1)) = s(s(1)+s(1))" and so on. But it is an informal proof, not a formal one, so to get to the mechanically verifiable level, you'd have to spell out a lot more details.
Yes but a "correct mathematical proof" only establishes truth relative to the axiom system used. Because how will you ever prove that the axioms are true? (That's why they're called axioms---you cannot prove them and just have to assume the're "true".) In other words, there's no such thing as "absolute truth". (This is what Hilbert meant when he defined mathematics as "Mathematics is that subject in which we do not know what we are talking about, nor whether what we say is true.")
Then you'd better check your facts ... there must be dozens (if not hundreds---erhhh, speaking about checking ones facts :-) ) of systems in which mathematical theorems are routinely proved (HOL, PVS, Coq, Mizar to name just a few)!
And what if you go up to someone and say "statement blah because here's a (very large) proof that my expert system generated, but which can be verified with a simple program which is just a few pages long"? Remember that *finding* a proof is hard (and hence requires human creativity / AI stuff) but *checking* that a proof is correct is easy (just a bit tedious when the proof is very large, and whom better to trust to do this job than a computer)?
That's what they said 50 years ago too ...
Maybe, one day, they'll implement a bit that indicates triple, quadruple, quintuple posts ... Sigh.
# rpm -Uvh red-carpet-0.9-0_helix_1.i386.rpm
only packages with major numbers <= 3 are supported by this version of RPM
error: red-carpet-0.9-0_helix_1.i386.rpm cannot be installed
Fantastic.
Maybe some day, I'll work out how to update my system enough in order to get this updater. *Sigh*
My version of the GPL says: You must cause any work that you distribute or publish, that in whole or in part contains or is derived from the Program or any part thereof, to be licensed as a whole at no charge to all third parties under the terms of this License. So in whatever way they modify, they have to license those modifications as GPL, and as far as I can work out, that means the source of those modifications must be distributed too ...
But then again, I an't no lawyer :-)
Maybe it's Stuff that matters then ...
ReiserFS *is* on the Mandrake CD. I installed my box (mandrake 7.1) without any ext2 partitions whatsoever, everything runs straight off reiserfs partitions.
There is a TeX plugin from IBM, it's called TexExplorer or something like that. By the way, I don't see how you can do a search in a bunch of text files for a particular kind of formula (``search for all the formulas containing 'something' to the power three inside an integral'') ... I hope this MathML stuff will make that kind of things possible.
Hm ... i don't agree completely. I skimmed the specs and there are also traditional (risc? don't remember exactly) cpu cores in the chip, so the bulk of the program can be coded the traditional way and only for the time critical part you use the special stuff ...
Every real programmer knows that the source is the documentation!
Seriously though, I don't really see the difference. If you make an undocumented change that is so drastic that everything crashes, documenting it doesn't really seem the remedy to me. Especially if you have a document-every-sneeze policy running, I don't see the advantage of having to search x Mb of docs about x/10 Mb of source code :-)
And the real lesson to be learnt here is that there are a lot of people out there who don't know better ... just give them their NT, give them their document-all policy, if they're happy with that, you probably don't want to bother to argue with them anyway :-)
> A program design that fails results in a few hours Me disagreeink. Like that bug in the mars explorer stuff where the one team used inches and the other centimeters ... that was *not* noticed after a few hours of programming methinks :-) So formal stuff could be of use also for software. Still don't know really what kind of formal stuff is to be used though (you can go pretty far in that direction).
However, it's interesting to note that when asked where he got all those wonderful names from, Asimov said he simply took usual names and twisted them a bit, and gave the example of Harry ->Hari ... if you like trivia ;-)
I don't know that much about physics, but the very last paragraph does seem the oddest of all: the mass of the spaceship is always zero, ergo the thing can reach superluminal speeds. Oh nice, at the very beginning, he says that the mass of a photon is always zero. So photons can reach superluminal speeds also, I suppose? ... heh :-)
Also, I'd like to see how big the radius r_s of that sphere turns out to be in practice
When the iridium satellite passes the field of view of the telescope, you see suddenly a very bright flash because the sattelite is rather reflective ... hence the name Iridium Flash :-)
Here at the university of Ghent, Belgium, there's a course in Operating Systems that involves doing stuff with CDROM-device drivers, a parallel port LED driver device, etc ... it's at http://www.elis.rug.ac.be/~kdb/best/ but presumably unfortunately most of it is in Dutch :-S
OK, but why is it that whenever a company gives away something for free they have to throw the buzz word 'Open Source' in somewhere? Giving away a compiler for free (as in 'beer') is of course something to be hurrayed upon, but the fact that their press release stuff has to throw in 'Open Source' is misleading, at least. So I'd say, let's pull out the beer, but not the champaign :-)
Maybe the patents are needed in some way to compensate for research costs, but I'd think that nowadays the life-time of patents is much too long. 25 years (or whatever) was maybe fine 100 years ago but nowadays technology of 10 years ago is obsolete, so I'd say that if patents are really a necessary evil (I don't like them anyway), the duration for computer-related patents should be shortened (5 years should be more than long enough to give the google guys their cash). Methinks.