Well, for one, they claim to implement an L4 kernel. Now I don't know exactly what it takes for a kernel to be an L4 kernel, but certainly it means certain behaviour can be expected. So if their spec makes the kernel not behave like an L4 kernel, it is buggy.
They had threee things: A formal specification, Haskell code and C code. They verified the C code against the formal specification by first verifying the Haskell code against the formal specification, and then the C code against the Haskell code. But that still only tells you that the formal specification, the Haskell code and the C code all three share the same set of bugs. I omitted the Haskell intermediate step because it doesn't give anything new.
Linux has more than ten million lines of code. Given that they needed 5 years for 12 persons to verify ten thousand lines of code, this means verifying the Linux kernel would give an estimated cost of 60,000 man-years. So even if they got a thousand people doing nothing else but verifying the Linux kernel, it would take then 60 years to finish.
Formal proofs are not unit tests. Unit tests test that certain values work correctly. Formal proofs show that the code works to the specification in all cases (modulo errors in the proof, of course). They of course cannot find bugs in the specification (which unit tests might, if they test what you thought the specification said, instead of what the specification really said).
What is there to get around? GÃfdel says that not every true statement is provable. They have not proven every true statement. Just one, that their kernel is correct.
No. They didn't prove that their kernel is correct. Just that their C code and their formalization of the specification share the same set of bugs.
A book written today ist most probably as valuable in twenty years as it is now. However what piece of software written 20 years ago is still useful for you?
You probably should always keep some encrypted porn on your computer. It's easily explained why you encrypted it (no one should find out that you have porn on your computer), and you can safely give the key to the police (as long as it's allowed porn of course, kiddy porn wouldn't work well:-)).
For convicting you, they would have to prove that there's a hidden partition.
Re:This isn't sensationalist, it's the truth
on
Leaving the GPL Behind
·
· Score: 5, Insightful
And in what way does the existence of that GPLed code make your work any harder than it would be if the code simply didn't exist? Or if it would exist, but buried deep inside some proprietary application whose source you won't even get to see, much less be allowed to use?
A business' motivation is not about restricting the user's freedom, it's about making sure that they get paid
Stop here. A business wants to be paid, period. If it needs to do work to get paid, it will do that work. But it will do that work in order to get money, not want the money because of the work. If they can get the money without the work, they will prefer that way (because work costs money). Releasing software under the GPL ensures they have to keep working in order to make money. Releasing under proprietary license means they can rest on the previous work (at least until someone else duplicated that amount of work, which, of course, means those others cannot put that work into innovation).
The viral nature of the GPL does make it harder to write programs. If you're going to claim it doesn't, then you're ignoring reality.
No. The GPL doesn't do anything to anyones programming abilities. Well, indirectly it makes it easier to write programs, by allowing you to learn from the program's source code.
And the way I hear things, those other (non-copyleft) licenses [...] don't get rewritten to forbid your business model.
Nor does the GPL. While there is a new GPL with new restrictions, any software you got under the old GPL you can continue to use under the old GPL. Of course this doesn't protect you from future versions from the same authors to be distributed under another license (and indeed, all software from the GNU project now is GPLv3), but you aren't protected from that with BSD or MIT/X licensed code either. The project owner could at one day decide he wants a completely different license (be it GPL, commercial, or whatever). So if you base your business model on BSD or MIT/X licensed code staying BSD or MIT/X in future versions, you may get surprises later on, too (as Transgaming will surely confirm). Indeed, with GPLed software you are better protected against license changes since for any change not already allowed by the license itself every single copyright holder has to agree to the licensing change. With a BSD license, the project maintainer can e.g. one day go proprietary without asking anyone, because he has the license to do so from any contributor. With the GPL, he cannot. Indeed, unless the licensing explicitly included the "or later" pass (the Linux kernel for example doesn't), he cannot even switch from GPLv2 to GPLv3 without every contributor agreeing (the FSF is a special case because people have to assign copyrights to get their code into GNU projects, so the FSF has greater freedom in licensing; however, the copyright transfer is coupled with a contract to keep the code free, so even the FSF couldn't make that code proprietary without all contributors explicitly agreeing, not even by writing a future "proprietary GPL").
Slashdot Mirror
Indeed even encrypted machines are pretty vulnerable to physical DoS attacks.
But it wasn't a real "no true scotsman" fallacy. After all, it didn't involve a scotsman. :-)
Well, for one, they claim to implement an L4 kernel. Now I don't know exactly what it takes for a kernel to be an L4 kernel, but certainly it means certain behaviour can be expected. So if their spec makes the kernel not behave like an L4 kernel, it is buggy.
Well, just initiate a DMA onto some memory the kernel uses, and you're toast.
I have two words for you:
denial.
And the second word is?
They had threee things: A formal specification, Haskell code and C code. They verified the C code against the formal specification by first verifying the Haskell code against the formal specification, and then the C code against the Haskell code. But that still only tells you that the formal specification, the Haskell code and the C code all three share the same set of bugs. I omitted the Haskell intermediate step because it doesn't give anything new.
Against whatever those who wrote the spec intended it to say.
Yes he does. From what I understand C is not "provable", or at least nigh impossible. With functional languages like ML, it is provable.
Isn't TFA about a proof of C code?
Linux has more than ten million lines of code. Given that they needed 5 years for 12 persons to verify ten thousand lines of code, this means verifying the Linux kernel would give an estimated cost of 60,000 man-years. So even if they got a thousand people doing nothing else but verifying the Linux kernel, it would take then 60 years to finish.
So what does the following Haskell program proof?
For spacecraft: AFAIK because the larger structures on the older chips are more robust against cosmic radiation.
Well, the bug in the driver might in principle cause the hardware to fail, and thus kill the kernel.
Formal proofs are not unit tests. Unit tests test that certain values work correctly. Formal proofs show that the code works to the specification in all cases (modulo errors in the proof, of course). They of course cannot find bugs in the specification (which unit tests might, if they test what you thought the specification said, instead of what the specification really said).
No. They didn't prove that their kernel is correct. Just that their C code and their formalization of the specification share the same set of bugs.
That's why you first write it in a formal language, then in a functional language.
A book written today ist most probably as valuable in twenty years as it is now. However what piece of software written 20 years ago is still useful for you?
So in the UK it is a crime to possess DRMed media? :-)
His assumption was that there is no data.
This means, you can be forced to do self-incrimination. What's next? Do we remove the right to remain silent? In dubio contra reo?
This is the UK. They already have removed the right to remain silent in the Justice and Public Order Act 1994.
I'm I the only one who at first misread the second 9 for an 8?
You probably should always keep some encrypted porn on your computer. It's easily explained why you encrypted it (no one should find out that you have porn on your computer), and you can safely give the key to the police (as long as it's allowed porn of course, kiddy porn wouldn't work well :-)).
For convicting you, they would have to prove that there's a hidden partition.
And in what way does the existence of that GPLed code make your work any harder than it would be if the code simply didn't exist? Or if it would exist, but buried deep inside some proprietary application whose source you won't even get to see, much less be allowed to use?
Stop here. A business wants to be paid, period. If it needs to do work to get paid, it will do that work. But it will do that work in order to get money, not want the money because of the work. If they can get the money without the work, they will prefer that way (because work costs money). Releasing software under the GPL ensures they have to keep working in order to make money. Releasing under proprietary license means they can rest on the previous work (at least until someone else duplicated that amount of work, which, of course, means those others cannot put that work into innovation).
No. The GPL doesn't do anything to anyones programming abilities. Well, indirectly it makes it easier to write programs, by allowing you to learn from the program's source code.
Nor does the GPL. While there is a new GPL with new restrictions, any software you got under the old GPL you can continue to use under the old GPL. Of course this doesn't protect you from future versions from the same authors to be distributed under another license (and indeed, all software from the GNU project now is GPLv3), but you aren't protected from that with BSD or MIT/X licensed code either. The project owner could at one day decide he wants a completely different license (be it GPL, commercial, or whatever). So if you base your business model on BSD or MIT/X licensed code staying BSD or MIT/X in future versions, you may get surprises later on, too (as Transgaming will surely confirm). Indeed, with GPLed software you are better protected against license changes since for any change not already allowed by the license itself every single copyright holder has to agree to the licensing change. With a BSD license, the project maintainer can e.g. one day go proprietary without asking anyone, because he has the license to do so from any contributor. With the GPL, he cannot. Indeed, unless the licensing explicitly included the "or later" pass (the Linux kernel for example doesn't), he cannot even switch from GPLv2 to GPLv3 without every contributor agreeing (the FSF is a special case because people have to assign copyrights to get their code into GNU projects, so the FSF has greater freedom in licensing; however, the copyright transfer is coupled with a contract to keep the code free, so even the FSF couldn't make that code proprietary without all contributors explicitly agreeing, not even by writing a future "proprietary GPL").