Unfortunately, as the grandparent points out, in languages that aren't as rigid as Java, its more difficult to fix unmaintainable code, since so much about the program is inferred at runtime. This makes static analysis for bugs and common refactoring patterns almost impossible, since each file of the source code is much less independent of other files.
If rigidity is so good, I assume all of these companies are moving over to Ada?
She also hates Arpaio for his tactics and flaunting of the law.
I thought it was pretty much a sheriff's job to flaunt the law? Oh, unless you mean "flout"... (this isn't spelling or grammar, it's semantics -- you may want to extend your sig).
Ahahahahaha. Yes, yes that's *exactly* what he's arguing. He couldn't *possibly* have meant white people are the benificiaries of a legacy of European colonization of Africa, the enslavement of those people in America, eventual manumission but disenfranchisement, and so on and so forth of gradual accessions to black people's rights, while nevertheless maintaining systemic white privilege.
Presumably not, because if he had meant that then it would have been just as much bullshit, because non-whites living in Europe and the USA today benefit pretty much as much from that "legacy of European colonization of Africa, the enslavement of those people in America, eventual manumission but disenfranchisement, and so on and so forth" as the white population does (mutatis mutandis for the European case), and where they don't it is rightly condemned as racism.
No, they do it because the OS doesn't have the necessary information. As I say, it's possible to write a program that is guaranteed to halt, but the OS doesn't know whether you've done that or not. So even if the halting problem could be solved, it still wouldn't be how the OS would determine that a program had gone zombie (eg, due to a hardware fault).
So when Chinese people discriminate against Indians on grounds of race (as they sometimes do in Hong Kong), you think it isn't racism because the Chinese are not white? What a narrow, parochial, racist attitude you have!
Thing is, any new thinking needs to be based on the tasks that users actually want to accomplish. The reason I use Firefox is because of the addins -- specifically Zotero, which I use daily. This new browser can rethink the concept as much as it likes; if it doesn't give me a means of citation management for free that is at least as good as I can get under Firefox (including integration with a word processing package at least as good as OpenOffice.org), I'm not interested. And I suspect that citation management is not high on the list of priorities when designing a web browser. The next user over might have an equally esoteric addon that they absolutely need. So I think RockMelt has an incredibly hard task -- any good ideas they come up with are likely to end up in Firefox soon after (with enough variation to get around UI patents), and we'll be able to use them without losing all the other stuff we need.
I know it's bad internet manners to use all caps, but I think this is an important point for all you children to hear:
There's NO SUCH THING as RACISM AGAINST WHITE PEOPLE.
Bullshit.
Though I digress, my point is that you can start complaining about racism against white people once people of color invade your homeland, enslave you, kill most everyone you know, then a couple of good-hearted ones finally manage to convince the others to leave you alone, but now you're left in crushing poverty in a place where most people hate you and your people.
My wife is non-white. She hasn't been enslaved, her friends and family have not been killed, she has not been left in crushing poverty in a place where most people hate her and her people. But she has been refused promotion on the grounds that the employer would never allow a non-white into a management position, and she has had a manager complain about having her on his team because he only wanted white men (she took that one to law on grounds of racial and sexual discrimination, and won). That's not what you describe, but it's still racism, and when it happens to white people (it does) then it's still racism. Your argument is a simple logical fallacy. You are arguing:
Premise 1: Invading your homeland, enslaving you, killing most everyone you know, being left in crushing poverty in a place where most people hate you and your people is racism.
Premise 2: What has happened to white people is not Invading their homeland, enslaving them, killing most everyone they know, being left in crushing poverty in a place where most people hate them and their people.
Conclusion: What has happened to white people is not racism.
Lets try another argument of exactly the same form:
Premise 1: Socrates was a man
Premise 2: Plato was not Socrates
Conclusion: Plato was not a man.
See why your argument doesn't hold up? It's called "denying the antecedant" -- look it up.
Two things. One is that "verifying whether a program has gone zombie" doesn't seem to be within the scope of an L4 kernel. The other is that kernels don't verify whether a program has "gone zombie" by doing static code analysis, which is what the halting problem is about, and if they do decide that a program has "gone zombie" they don't do it on the basis that it will never terminate, only that it hasn't terminated within a reasonable timescale, so again the halting problem doesn't apply.
It's an important property (and not the same property as "contains bugs" -- or even as "doesn't contain bugs"), but unless you can specify what it means in computational terms, precisely how is Rice's theorem going to apply?
No it doesn't. The information that is external to the program code can (and typically does) include assertions about the code that cannot be computed but can be proven mathematically. And it doesn't matter that it can't be automated away, because it isn't automated (it wouldn't take so long if it were).
The spam-fighting method is to build a sufficient number of email accounts that work that way and start black-listing every email that does NOT work that way and/or is not on your contact list. Not that hard to do.
Yeah, maybe you can afford to send new customers to/dev/null, but I sure can't.
Well, ok, so it has to provide address spaces, threads, scheduling, and synchronous inter-process communication (but not in any particular way, AIUI). I think that checking that those are included in the spec could be pretty reliably assured by review, don't you?
The study of the halting problem taught us that certain categories of algorithms cannot be formally proved to do certain things. Work on incompleteness tells us that we know algorithms must exist that fit that category.
The question, really, is whether the algorithms in and design of operating systems can be done in such a way that we don't run into incompleteness and halting-problem issues within the constraints of what we are trying to achieve
And the answer in this case is pretty certainly "Yes, we can"; the tasks you can't do without running into halting or incompleteness issues are pretty esoteric and well outside the sort of thing an OS kernel would sensibly be called on to do.
Who cares what they intended? All the users of the kernel care about is what is actually specified. This isn't a top-level application where there's a mapping to real world intentions ("prevent the aircraft from crashing"), this is a building block, and the builders need to decide whether it's the right size and shape for whatever they are building.
Why so? They have precisely specified what the kernel is to do, and have proven that it does it. Whether it's what you want it to do isn't their question, it's yours.
At least one of the formal specification languages (can't remember whether it's Z or VDM) is based on Russel & Whitehead's theory of types, which isn't omega complete. That prevents the possibility of self-reference which would lead it to fall foul of Godel's incompleteness theorem. It makes the expression of certain propositions impossible (For example, you can't construct "the set of all sets that don't contain themselves" because types are heirarchical, so the type of the members of the set would be different from the type of the set that contains them. You'd have to construct "the set2 of all set1s that don't contain themselves" and asking if the set is a member of itself would be a type error -- it's a set2, and can only contain set1s).
The theory of types turned out to be too weak to build mathematics on, but it turns out to be plenty strong enough for any real-world program specifications.
Nope. The halting problem only applies to arbitrary programs. It's simple to write programs of arbitrary complexity that are guaranteed to halt (as long as what you want to do is algorithmic), it just isn't simple to tell if the program you have been given is one of those programs unless you can see the evidence that the programmer has done that.
Well, there are some theoretical problems with this idea. The halting problem is trivial to prove insolvable, and it turns out that it's possible to generalise this proof and demonstrate that it's not possible to prove any complex properties of arbitrary programs.
Irrelevant. This is not an arbitrary program, this is one that has been specifically written to be provable, and there have been techniques for doing that for at least 20 years, because I was taught them 20 years ago. If every loop has a loop variant specified -- a finite positive integer that is proven to decrease on every pass of the loop -- then all loops are guaranteed to terminate (the variant can't go on decreasing indefinitely) and so the program is guaranteed to halt. Given an arbitrary program you might not be able to work out loop variants, but if you only write code for which you have worked out the loop invariants then the halting problem does not apply to your code. As you say:
it's comparatively easy to write the program and the proof concurrently.
...which is what they will have done, so the halting problem won't be a problem in this case. (Of course, as an OS Kernel it presumably has an outer loop that isn't supposed to terminate, but you need to make sure that everything operating within that loop does terminate).
Oh, and the other problem with this model is the concept of the trusted computing base. If the kernel is written in a high-level language, then the compiler also needs to be verified for the verification to be worthwhile.
Yes, this one is an issue -- and what do you verify the compiler against, if the language doesn't have formally defined semantics.
Even if we have a perfect kernel, it won't insulate us from bugs in the software running on top of that kernel, so do we really gain much?
I guess for mission critical apps the answer could be yes... But for every-day computing?? On my desktop I have more trouble with Firefox crashing than I do the OS! (Yes I run linux).
The advantage for everyday computing is that because of its use in the mission critical software you survive your flight and can continue with your everyday computing.
Prove the spec against what? The spec just says "This is what the kernel does". It's up to the client to decide whether what the kernel does is any use for them.
"Usable?" is a sensible question, but "bugfree?" is not. It's a meaningless question at the level of an OS kernel. You are wrongly thinking at the application level, not at the kernel level. The kernel gives you some guaranteed behaviour. If that behavour provides what you want then it's usable. If it doesn't then it's not. Neither case is a "bug".
Slashdot Mirror
Unfortunately, as the grandparent points out, in languages that aren't as rigid as Java, its more difficult to fix unmaintainable code, since so much about the program is inferred at runtime. This makes static analysis for bugs and common refactoring patterns almost impossible, since each file of the source code is much less independent of other files.
If rigidity is so good, I assume all of these companies are moving over to Ada?
She also hates Arpaio for his tactics and flaunting of the law.
I thought it was pretty much a sheriff's job to flaunt the law? Oh, unless you mean "flout"... (this isn't spelling or grammar, it's semantics -- you may want to extend your sig).
Ahahahahaha. Yes, yes that's *exactly* what he's arguing. He couldn't *possibly* have meant white people are the benificiaries of a legacy of European colonization of Africa, the enslavement of those people in America, eventual manumission but disenfranchisement, and so on and so forth of gradual accessions to black people's rights, while nevertheless maintaining systemic white privilege.
Presumably not, because if he had meant that then it would have been just as much bullshit, because non-whites living in Europe and the USA today benefit pretty much as much from that "legacy of European colonization of Africa, the enslavement of those people in America, eventual manumission but disenfranchisement, and so on and so forth" as the white population does (mutatis mutandis for the European case), and where they don't it is rightly condemned as racism.
so the system is now supported on the backs of the ignorant.
And the ethical. And those nervous of $1.92 million lawsuits.
No, they do it because the OS doesn't have the necessary information. As I say, it's possible to write a program that is guaranteed to halt, but the OS doesn't know whether you've done that or not. So even if the halting problem could be solved, it still wouldn't be how the OS would determine that a program had gone zombie (eg, due to a hardware fault).
So when Chinese people discriminate against Indians on grounds of race (as they sometimes do in Hong Kong), you think it isn't racism because the Chinese are not white? What a narrow, parochial, racist attitude you have!
Thing is, any new thinking needs to be based on the tasks that users actually want to accomplish. The reason I use Firefox is because of the addins -- specifically Zotero, which I use daily. This new browser can rethink the concept as much as it likes; if it doesn't give me a means of citation management for free that is at least as good as I can get under Firefox (including integration with a word processing package at least as good as OpenOffice.org), I'm not interested. And I suspect that citation management is not high on the list of priorities when designing a web browser. The next user over might have an equally esoteric addon that they absolutely need. So I think RockMelt has an incredibly hard task -- any good ideas they come up with are likely to end up in Firefox soon after (with enough variation to get around UI patents), and we'll be able to use them without losing all the other stuff we need.
I know it's bad internet manners to use all caps, but I think this is an important point for all you children to hear:
There's NO SUCH THING as RACISM AGAINST WHITE PEOPLE.
Bullshit.
Though I digress, my point is that you can start complaining about racism against white people once people of color invade your homeland, enslave you, kill most everyone you know, then a couple of good-hearted ones finally manage to convince the others to leave you alone, but now you're left in crushing poverty in a place where most people hate you and your people.
My wife is non-white. She hasn't been enslaved, her friends and family have not been killed, she has not been left in crushing poverty in a place where most people hate her and her people. But she has been refused promotion on the grounds that the employer would never allow a non-white into a management position, and she has had a manager complain about having her on his team because he only wanted white men (she took that one to law on grounds of racial and sexual discrimination, and won). That's not what you describe, but it's still racism, and when it happens to white people (it does) then it's still racism. Your argument is a simple logical fallacy. You are arguing:
Lets try another argument of exactly the same form:
See why your argument doesn't hold up? It's called "denying the antecedant" -- look it up.
Two things. One is that "verifying whether a program has gone zombie" doesn't seem to be within the scope of an L4 kernel. The other is that kernels don't verify whether a program has "gone zombie" by doing static code analysis, which is what the halting problem is about, and if they do decide that a program has "gone zombie" they don't do it on the basis that it will never terminate, only that it hasn't terminated within a reasonable timescale, so again the halting problem doesn't apply.
It's an important property (and not the same property as "contains bugs" -- or even as "doesn't contain bugs"), but unless you can specify what it means in computational terms, precisely how is Rice's theorem going to apply?
No it doesn't. The information that is external to the program code can (and typically does) include assertions about the code that cannot be computed but can be proven mathematically. And it doesn't matter that it can't be automated away, because it isn't automated (it wouldn't take so long if it were).
The spam-fighting method is to build a sufficient number of email accounts that work that way and start black-listing every email that does NOT work that way and/or is not on your contact list. Not that hard to do.
Yeah, maybe you can afford to send new customers to /dev/null, but I sure can't.
Oh, The Who was far more than just Pete Townsend, although he was a significant part.
Well, ok, so it has to provide address spaces, threads, scheduling, and synchronous inter-process communication (but not in any particular way, AIUI). I think that checking that those are included in the spec could be pretty reliably assured by review, don't you?
The study of the halting problem taught us that certain categories of algorithms cannot be formally proved to do certain things. Work on incompleteness tells us that we know algorithms must exist that fit that category.
The question, really, is whether the algorithms in and design of operating systems can be done in such a way that we don't run into incompleteness and halting-problem issues within the constraints of what we are trying to achieve
And the answer in this case is pretty certainly "Yes, we can"; the tasks you can't do without running into halting or incompleteness issues are pretty esoteric and well outside the sort of thing an OS kernel would sensibly be called on to do.
Who cares what they intended? All the users of the kernel care about is what is actually specified. This isn't a top-level application where there's a mapping to real world intentions ("prevent the aircraft from crashing"), this is a building block, and the builders need to decide whether it's the right size and shape for whatever they are building.
Why so? They have precisely specified what the kernel is to do, and have proven that it does it. Whether it's what you want it to do isn't their question, it's yours.
At least one of the formal specification languages (can't remember whether it's Z or VDM) is based on Russel & Whitehead's theory of types, which isn't omega complete. That prevents the possibility of self-reference which would lead it to fall foul of Godel's incompleteness theorem. It makes the expression of certain propositions impossible (For example, you can't construct "the set of all sets that don't contain themselves" because types are heirarchical, so the type of the members of the set would be different from the type of the set that contains them. You'd have to construct "the set2 of all set1s that don't contain themselves" and asking if the set is a member of itself would be a type error -- it's a set2, and can only contain set1s).
The theory of types turned out to be too weak to build mathematics on, but it turns out to be plenty strong enough for any real-world program specifications.
Nope. The halting problem only applies to arbitrary programs. It's simple to write programs of arbitrary complexity that are guaranteed to halt (as long as what you want to do is algorithmic), it just isn't simple to tell if the program you have been given is one of those programs unless you can see the evidence that the programmer has done that.
Well, there are some theoretical problems with this idea. The halting problem is trivial to prove insolvable, and it turns out that it's possible to generalise this proof and demonstrate that it's not possible to prove any complex properties of arbitrary programs.
Irrelevant. This is not an arbitrary program, this is one that has been specifically written to be provable, and there have been techniques for doing that for at least 20 years, because I was taught them 20 years ago. If every loop has a loop variant specified -- a finite positive integer that is proven to decrease on every pass of the loop -- then all loops are guaranteed to terminate (the variant can't go on decreasing indefinitely) and so the program is guaranteed to halt. Given an arbitrary program you might not be able to work out loop variants, but if you only write code for which you have worked out the loop invariants then the halting problem does not apply to your code. As you say:
it's comparatively easy to write the program and the proof concurrently.
...which is what they will have done, so the halting problem won't be a problem in this case. (Of course, as an OS Kernel it presumably has an outer loop that isn't supposed to terminate, but you need to make sure that everything operating within that loop does terminate).
Oh, and the other problem with this model is the concept of the trusted computing base. If the kernel is written in a high-level language, then the compiler also needs to be verified for the verification to be worthwhile.
Yes, this one is an issue -- and what do you verify the compiler against, if the language doesn't have formally defined semantics.
Even if we have a perfect kernel, it won't insulate us from bugs in the software running on top of that kernel, so do we really gain much? I guess for mission critical apps the answer could be yes... But for every-day computing?? On my desktop I have more trouble with Firefox crashing than I do the OS! (Yes I run linux).
The advantage for everyday computing is that because of its use in the mission critical software you survive your flight and can continue with your everyday computing.
Prove the spec against what? The spec just says "This is what the kernel does". It's up to the client to decide whether what the kernel does is any use for them.
no. another theorem tells that you can never verify that a code is bug free (it may be bug free, but you cannot prove it)
[Citation needed]
"Usable?" is a sensible question, but "bugfree?" is not. It's a meaningless question at the level of an OS kernel. You are wrongly thinking at the application level, not at the kernel level. The kernel gives you some guaranteed behaviour. If that behavour provides what you want then it's usable. If it doesn't then it's not. Neither case is a "bug".