Yes. Tire roar isn't going away, and it's quite loud as-is on a road with a decent speed limit [...] So that covers highways, arterials and most collectors.
Where I live, the speed limit for local roads is 50km/h normally, or 40 around schools. (That's 25 m/h for those who are still living in the 19th century.) Add some environmental noise, and all you can hear of a car at that speed is the engine.
This message has no content, but is part of an ongoing experiment to see if it's true that you can get a +1 (in this case, Funny) for quoting the phrase "Before you mod me down".
You can't type my name into any search engine and get a photo of my house. (I have an unlisted number.)
I have to agree that she crossed a moral line, whether or not it was a legal one. What a police officer does when on duty should be public. When they're off-duty, it should be private.
The details are on NICTA's web site. Basically, they have verified that the C source code accurately implements a formal model of the L4 spec. They have not, for example, verified that the C compiler accurately implements the formal subset of C.
Formally verified compilers are still an active research area. Formally verified hardware has at least been around for a while, at least for chips smaller than VLSI.
What you'd like is for the entire stack to be formally verifiable, but we're a long way off that at the moment. Remember, it's only been in the last few years that assisted theorem provers like Isabelle and Coq have been up to the job.
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?
Right, and this is probably the most important point.
The primary limitation to proving programs correct is not the halting problem, not the inability of theorem provers to understand your C code and not Rice's theorem. It's that the desired behaviour of your program isn't well-specified in the first place. Moreover, a formal specification for most nontrivial programs is likely to be as hard to write and debug as the program itself, or even harder.
You may want to bear in mind, for example, that L4 contains no peripheral drivers.
(Disclaimer: I work for NICTA. Different lab, though.)
I'm not sure that I agree. The multi-universe interpretation suffers from a very serious, IMO fatal, problem in lay-explanatory power, which is that it's difficult to picture several split universes "interfering" to cancel each other out.
They are supposed to make the claim against the area for which their language is most appropriate.
Then you run into the opposite extreme, which is that some programming languages develop an implicit theory about what they are "for" and then get stereotyped in that domain. You know, C is "for" systems programming on Unix. Java is "for" deploying untrusted applets over the Internet. Perl is "for" batch/reporting jobs that require a slightly thicker layer of glue than a shell script. PHP is "for" web scripting jobs that are slightly more demanding than SSI. Haskell is "for" writing its own compiler in.
Usually the answer is one that's difficult to compute but easy to check, such as any problem in NP. Checking that you have a factor of a number is much easier than producing a factor, and checking that a proof is correct is much easier than producing a correct proof.
The other option is to simply run it more than once. If you have an algorithm which is wrong 1% of the time (and that 1% is uncorrelated to the "input"), then if you run it ten times, the chance that all of them are wrong is extremely small.
Having said that, the "many universes" model is, according to most quantum mechanics, not an accurate picture. It's better to think of quantum algorithms as being probabilistic algorithms that works with quantum probability theory rather than classical probability theory.
You must admit, though, that religion provides a convenient and inexplicably politically-correct excuse for fostering repressive government and xenophobic belligerence.
The fear of terrorism is far more convenient, don't you think? Greater atrocities were committed in the last decade in the name of "freedom" and "democracy" than most religious fundamentalists could ever accomplish.
Of course, all the elements were in place before November 2003. Notably absente from the patent is any reference to prior art by Kevin Marks or Dave Winer. Marks' RSS2iPod script, for example, was released in October of that year.
The only claim that post-dates November 2003 that I can see is that clients (along with things like intelligent cache management) have since been implemented directly on non-PC portable devices. Most sane people would consider that obvious: as portable devices get more powerful, more of the processing inevitably gets moved there.
About 80% of the software engineering market is about fixing the impedance mismatch between half a dozen off-the-shelf legacy systems and getting them to work together. This is the world of customer requirements, filing bugs with vendors, business rules, sorting out SQL variants,.NET and TPS reports.
The other 20% is in writing those systems or stuff you can't get off the shelf for people who really need it. This is the world of R&D, resource management, high-performance, real-time, scientific, numeric, visualisation, embedded, crypto, machine learning, metal, speed and danger.
Now, which of these do you want to do for a living?
Last year, I was writing firmware for nanotech devices. I implemented shell sort. Do you remember shell sort? I'm glad I had a broad CS education which told me what it shell sort was, because it was exactly the right trade-off (small-to-medium amounts of data, with practically no working memory to spare).
This year I'm helping find disease outbreaks before they happen. I had to implement a suffix array. Do you remember what a suffix array is and what it's for? I didn't learn this as an undergrad (that was a while ago), but thanks to my broad CS education, I knew what I needed to find out.
A pilot will probably never have to safely ditch an airliner in the ocean at any point in their career. But there's no way in hell that I'm hiring one that doesn't know how to do it.
The Disney version of the history of animation in the United States is pure mythology.
Walt had actually been making animation for 8 years before Mickey came along, some of them quite popular the Alice comedies and Oswald the Lucky Rabbit. In addition, Steamboat Willie was actually the third Mickey Mouse cartoon. It was just the first with synchronised sound (the earlier two later had sound added).
In the real world you can use any software you wish.
Oh, you poor, naive person.
Let me introduce myself. I'm from the real world. Let me explain how things happen here.
We have to deal with tricky problems. Sometimes, a function has more than one formal integral, and some forms are more appropriate than others in different situations. Good luck coaxing your CAS into giving you exactly what you want.
We have to deal with deadlines. If you can solve a problem in two minutes on paper, that's usually quicker than loading up most software packages and trying to get your equation into the syntax of the system. (Naturally, no two systems use the same syntax.)
Even worse, we have to deal with software licensing. Mathematica and Matlab ain't cheap. Software vendors try to argue that you're a commercial institution, not a research institution, so they can gouge you for licence fees. Cross your fingers and hope that there is a small enough number of people using the software concurrently so that you can get in. Otherwise, you're screwed.
Rote learning can't teach you how to think it can only force feed you the answer and make you throw up answers on cue.
This isn't "rote learning", it's drilling you on the method. The reason why you're required to "show all working" is to show that you've learned that method, even if there are simpler methods which work on that problem. That way, when you come across a real problem in the wild for which that method is most appropriate, you'll be ready for it.
The purpose of an exam is not to show how clever you are at solving problems, it's to show how much of the material you've learned.
The majority of users probably have no idea what DRM is and are thus unaffected.
Right. The point is that those who are affected by it are the ones who break the DRM.
Of the latest generation of games consoles, there is only one whose copy protection has not been broken. It's also the only one whose manufacturer allows (and explicitly blesses) the installation of Linux without breaking anything. This is not a coincidence.
Well, in that case, you should know that Russia has a very long track record in keeping obsolete technology going for a very long time. Hell, they still use R7s.
You jest, but I'm pretty much convinced that most good Java programmers use Java despite the language, rather than because of it. The real value in Java isn't the language, but the environment (VM, libraries etc).
Brisbane is the capital (and largest) city in the state of Queensland. The nearest cities are Mackay and Townsville; it's about half-way between them, about 100km each way.
More crucially, though, Bowen is in the middle of a fairly major tourist area, given that it's right next to the Great Barrier Reef. It's also had a larger influx of tourists recently because bits of Baz Lurhmann's Great Patriotic Extravagance were filmed there.
I'm an Aussie living in Melbourne so I get the joke.
Melburnians really shouldn't make jokes about how people in other places complain about the weather. We in Melbourne complain about how cold it is when the sign on the silo says eleven degrees.
Slashdot Mirror
Yes. Tire roar isn't going away, and it's quite loud as-is on a road with a decent speed limit [...]
So that covers highways, arterials and most collectors.
Where I live, the speed limit for local roads is 50km/h normally, or 40 around schools. (That's 25 m/h for those who are still living in the 19th century.) Add some environmental noise, and all you can hear of a car at that speed is the engine.
This message has no content, but is part of an ongoing experiment to see if it's true that you can get a +1 (in this case, Funny) for quoting the phrase "Before you mod me down".
You can't type my name into any search engine and get a photo of my house. (I have an unlisted number.)
I have to agree that she crossed a moral line, whether or not it was a legal one. What a police officer does when on duty should be public. When they're off-duty, it should be private.
Didn't help that I was suffering at that time from an undiagnosed disease (Addison's) that left me fatigued.
I first read that as a joke at Addison-Wesley's expense. Just thought you'd like to know.
The details are on NICTA's web site. Basically, they have verified that the C source code accurately implements a formal model of the L4 spec. They have not, for example, verified that the C compiler accurately implements the formal subset of C.
Formally verified compilers are still an active research area. Formally verified hardware has at least been around for a while, at least for chips smaller than VLSI.
What you'd like is for the entire stack to be formally verifiable, but we're a long way off that at the moment. Remember, it's only been in the last few years that assisted theorem provers like Isabelle and Coq have been up to the job.
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?
Right, and this is probably the most important point.
The primary limitation to proving programs correct is not the halting problem, not the inability of theorem provers to understand your C code and not Rice's theorem. It's that the desired behaviour of your program isn't well-specified in the first place. Moreover, a formal specification for most nontrivial programs is likely to be as hard to write and debug as the program itself, or even harder.
You may want to bear in mind, for example, that L4 contains no peripheral drivers.
(Disclaimer: I work for NICTA. Different lab, though.)
I'm not sure that I agree. The multi-universe interpretation suffers from a very serious, IMO fatal, problem in lay-explanatory power, which is that it's difficult to picture several split universes "interfering" to cancel each other out.
They are supposed to make the claim against the area for which their language is most appropriate.
Then you run into the opposite extreme, which is that some programming languages develop an implicit theory about what they are "for" and then get stereotyped in that domain. You know, C is "for" systems programming on Unix. Java is "for" deploying untrusted applets over the Internet. Perl is "for" batch/reporting jobs that require a slightly thicker layer of glue than a shell script. PHP is "for" web scripting jobs that are slightly more demanding than SSI. Haskell is "for" writing its own compiler in.
Usually the answer is one that's difficult to compute but easy to check, such as any problem in NP. Checking that you have a factor of a number is much easier than producing a factor, and checking that a proof is correct is much easier than producing a correct proof.
The other option is to simply run it more than once. If you have an algorithm which is wrong 1% of the time (and that 1% is uncorrelated to the "input"), then if you run it ten times, the chance that all of them are wrong is extremely small.
Having said that, the "many universes" model is, according to most quantum mechanics, not an accurate picture. It's better to think of quantum algorithms as being probabilistic algorithms that works with quantum probability theory rather than classical probability theory.
The fear of terrorism is far more convenient, don't you think? Greater atrocities were committed in the last decade in the name of "freedom" and "democracy" than most religious fundamentalists could ever accomplish.
Of course, all the elements were in place before November 2003. Notably absente from the patent is any reference to prior art by Kevin Marks or Dave Winer. Marks' RSS2iPod script, for example, was released in October of that year.
The only claim that post-dates November 2003 that I can see is that clients (along with things like intelligent cache management) have since been implemented directly on non-PC portable devices. Most sane people would consider that obvious: as portable devices get more powerful, more of the processing inevitably gets moved there.
About 80% of the software engineering market is about fixing the impedance mismatch between half a dozen off-the-shelf legacy systems and getting them to work together. This is the world of customer requirements, filing bugs with vendors, business rules, sorting out SQL variants, .NET and TPS reports.
The other 20% is in writing those systems or stuff you can't get off the shelf for people who really need it. This is the world of R&D, resource management, high-performance, real-time, scientific, numeric, visualisation, embedded, crypto, machine learning, metal, speed and danger.
Now, which of these do you want to do for a living?
Last year, I was writing firmware for nanotech devices. I implemented shell sort. Do you remember shell sort? I'm glad I had a broad CS education which told me what it shell sort was, because it was exactly the right trade-off (small-to-medium amounts of data, with practically no working memory to spare).
This year I'm helping find disease outbreaks before they happen. I had to implement a suffix array. Do you remember what a suffix array is and what it's for? I didn't learn this as an undergrad (that was a while ago), but thanks to my broad CS education, I knew what I needed to find out.
A pilot will probably never have to safely ditch an airliner in the ocean at any point in their career. But there's no way in hell that I'm hiring one that doesn't know how to do it.
Sorry, a chrome sphere hovering over an infinite chess board doesn't count as a "movie".
The Disney version of the history of animation in the United States is pure mythology.
Walt had actually been making animation for 8 years before Mickey came along, some of them quite popular the Alice comedies and Oswald the Lucky Rabbit. In addition, Steamboat Willie was actually the third Mickey Mouse cartoon. It was just the first with synchronised sound (the earlier two later had sound added).
Oh, you poor, naive person.
Let me introduce myself. I'm from the real world. Let me explain how things happen here.
We have to deal with tricky problems. Sometimes, a function has more than one formal integral, and some forms are more appropriate than others in different situations. Good luck coaxing your CAS into giving you exactly what you want.
We have to deal with deadlines. If you can solve a problem in two minutes on paper, that's usually quicker than loading up most software packages and trying to get your equation into the syntax of the system. (Naturally, no two systems use the same syntax.)
Even worse, we have to deal with software licensing. Mathematica and Matlab ain't cheap. Software vendors try to argue that you're a commercial institution, not a research institution, so they can gouge you for licence fees. Cross your fingers and hope that there is a small enough number of people using the software concurrently so that you can get in. Otherwise, you're screwed.
This isn't "rote learning", it's drilling you on the method. The reason why you're required to "show all working" is to show that you've learned that method, even if there are simpler methods which work on that problem. That way, when you come across a real problem in the wild for which that method is most appropriate, you'll be ready for it.
The purpose of an exam is not to show how clever you are at solving problems, it's to show how much of the material you've learned.
Right. The point is that those who are affected by it are the ones who break the DRM.
Of the latest generation of games consoles, there is only one whose copy protection has not been broken. It's also the only one whose manufacturer allows (and explicitly blesses) the installation of Linux without breaking anything. This is not a coincidence.
Well, in that case, you should know that Russia has a very long track record in keeping obsolete technology going for a very long time. Hell, they still use R7s.
You jest, but I'm pretty much convinced that most good Java programmers use Java despite the language, rather than because of it. The real value in Java isn't the language, but the environment (VM, libraries etc).
It's "Ayr".
Brisbane is the capital (and largest) city in the state of Queensland. The nearest cities are Mackay and Townsville; it's about half-way between them, about 100km each way.
More crucially, though, Bowen is in the middle of a fairly major tourist area, given that it's right next to the Great Barrier Reef. It's also had a larger influx of tourists recently because bits of Baz Lurhmann's Great Patriotic Extravagance were filmed there.
Yeah, Paris really took public transport seriously in medieval times.
Melburnians really shouldn't make jokes about how people in other places complain about the weather. We in Melbourne complain about how cold it is when the sign on the silo says eleven degrees.
I don't make computer hardware, so on a non-legal reading, I'd say I'm in the clear.
Just goes to show that legalese is a different language.
Like I said, it depends on what you're doing and on all other things being equal.