I have to say that you are one of the more reasonable proof-advocates I've seen. You seem to have the kind of pragmatic approach to proofs that don't have any problems with.
My point is that a formal proving process is not necessarily better than an ad-hoc code verification process in the respect that just because you can (using a tool, which we for argument's sake can assume to be bug-free) prove that your program conforms to a formally written specification doesn't mean that the code will work. All you have proved is that it conforms to the specification. You simply moved the potential for bugs from the implementation to the formal specification. The problem is that the formal specification is just as or even more complicated to read and write than the implementation itself. Not to mention the fact that very few people know how to express software designs in a mathematical notation rather than code, and even fewer people a actually prefer that notation to normal computer code.
I think your last paragraph is the most correct one. The real benefit of the formal proving process is that it forces the reviewer to actually go through the code. There is no way to just gloss over the code.
Arguably it's not really relevant either. "proving" a software program only proves that the programs conforms to the spec. Now who proves the spec? And who proves the proof?
At the end of the day you're going to end up with a hell of a lot more documentation and proofs that no one will ever read, and the system won't be much better than the system that wasn't proven.
I think it's a quantum leap. Not because of the snapshotting or error checking, but the thing that really makes ZFS a completely different beast is that it is (to my knowledge) the first file system (or should I say "storage technology"?) that actually joins two traditionally separate concepts: file systems and volume management.
Thanks to this, a lot of interesting stuff becomes possible, such as the fast file system creation which is demonstrated in this very cool demo.
If you don't consider ZFS a quantum leap in file system technology, I wonder what it would take for you to use that expression (set aside for the moment the people who argue that "wuantum leap" should in fact mean the opposite:-) ).
I think the major advantage is the fast snapshotting and cloning. It uses copy-on-write so that it doesn't take more space than what you actually change.
Imagine being able to take really fast working copies of whatever you're doing and be able to simple use the old versions by cd'ing to the old clone.
That's certainly what I would use ZFS for. The rest of the stuff, pooling and mirroring and stuff is less interesting in my laptop.:-)
Assuming your numbers are right, and you stack the hard drivers well (I've assumed an extra 50% to allow for cooling), your array would occupy 14377 cubic metres.
Assuming a standard 19-inch rack which holds 96 drives, you'd need 256147 racks to hold the drives. Given a floor size of 0.16 square metres per rack, you'd end up with 3.779 football fields worth of racks.
I leave it to someone else to calculate the heat dissipation from this array.
Not many comments yet, but most seem to be very negative of the idea.
I wonder why. In fact, I think this is a great idea. It gives the consumer a chioce. Either he won't care one bit about this "interactive" commercial and keep fast-forwarding through them or he can get involved and watch the commercial thoroughly, adding value for himself as well as the supplier of the ad.
This is the way a free market is supposed to work. If the consumer doesn't want to watch the commercials, add some value to them. No one is still not forcing you to watch the commercial.
I definitiely prefer this to some other sceme where the cable companies block the fast-forward button during the commericals like they do on DVD's.
By the time I'm writing this, there are already a lot of replies, most of them saying the same thing: "that's what real life is, it's entertainment not teaching, yadda yadda", so I doubt that many will bother to read this.
In any case, this is one of the reasons why I stopped playing WoW after about a week.
You can't become good.
You can become experienced, you can invest a lot of time and thus get a higher experience level, you can build a large network of people to chat with... But you can't become a skilled WoW player.
Just about the only skill you can obtain is learning all the maps and the missions. The rest of the time is being spent doing the same thing over and over again in order to raise your XP. Even games that I utterly dislike, such as CS, allows you to become skilled. Actually, most glames do, but not the MMORPGs. I honestly don't understand why. Perhaps it's because most people are not prepared to practice something? Perhaps WoW is just an alternative to planting oneself in front of the TV, watching MTV? (i.e. no intelligence required). I don't know, and by now I don't really think I care.
Now that I'm writing a post about WoW, I have to add my pet peeve as wel:
Playing WoW, it feels like I'm trapped in the Twilight Zone. I walk around in a living world, things happen all around me, but no one can really see me. I'm like a walking shadow, somehow being able to touch things, but still not. Anything I do have absolutely zero effect on the world. It really kills the immersion for me when an NPC tells me that I need to save the village by killing this or that monster. I do it, I arrive in a triumphant return... but... No... Wait... Nothing changed! The village is apparently still held in the grasp of this monster, since the very same person is still handing out the same quest to other players. I'm still the same no-one I was before, altough with a couple of more experience points, and the world laughts in my face saying: "Don't think you can be someone special. You're always doomed to be a boring no-one, and you'll never affect the world".
I know it was a joke, but if had had mod points I'd given you +1 insightful on that one.
The problem with fingerprints is that it's inherently a very insecure way of authentication for two reasons:
Firstly, you can't change it if it leaks out. A password or a credit card number can be easily changed and the damage minimised in case of an information leak. Doing this with a fingerprint is much harder.
Secondly, the fingerprint is very hard to keep secret. Your body has this annoying ability to leave copies of your identification token all over the place, very easy for anyone to pick up. If you were worried about the ability to scan proximity tags (RFID), then you should be really scared about the use of fingerprints as authentication tokens.
If you don't believe me how easy it is to pick up, read this about how to make a copy of ones fingerprint using common household items.
Unfortunately talk radio is missing out on this new technology entirely thanks to bumper music agreements with the RIAA and some unions. One of the few to get around it is the well known Rush Limbaugh, but he can do it largely because of his popularity.
Here in Sweden, talk radio is all public service. The commercial stations only broadscast back-to-back "hit" music. Since I hate the commercial crap music, I never listen to the commercial stations.
Anyway, even the good shows on public service radio mix their shows with yet more "hit" music making them rather painful to listen to. You're enjoying a fun comedy show and all of a sudden: Bang! You get hit over the head with Britney Spears.
Now, the good thing is that public service radio has started to make their shows available as podcasts. I download them via ITMS. Because of (or shall I say thanks to) the music agreemets, all the commercial music is edited out of the shows. I couldn't be happier. I finally get to listen to the show the way I want it and I don't even have to fast-forward. In this particular case, I hope they don't sign a music distribution agreement for the podcasts. Most of the people I've talked to about this agree as well.
If I really want the shows mixed with music, I can just switch to one of my other thousands of songs I already have on my iPod.
While I have no doubt that given the chance, Apple would behave just as bad as MS, I just can't see why would in any way want to band up with MS at this time.
First of all, Apple is actively competing against MS in a way that even surprises many Mac fanatics, for example by releasing Pages in addition to Keynote. Apple losing MS Office would not be very good for their business. While in a somewhat different segment, the media player competition between Apple and MS is also quite fierce.
Secondly, Linux does not pose any major threat against MS and Apple at this time. Granted, MS loses users to Linux but Apple is stealing Linux users to OSX. I fail to see what MS has to contribute here.
I'm quite certain that the new code verification algorithm has been theoretically proven.
What is going to be tested is the implementation, not the theory behind the algorithm, however. It doesn't really matter how well proven the algorithm is if the implementation has a bug (which could caused by a typo for example).
Code proving is a nice theoretical excersise, but don't for a second believe that just because some code has been put through a formal proof that it cannot contain bugs.
"ergonomic" devices are not ergonomic at all
on
Ergonomic Mice Reviewed
·
· Score: 2, Interesting
Seriously... What's the deal with all of these "ergonomic" pointing devices?
Most of them are big as houses are requires you to move your entire hand to move the damn thing around the desk. If anything, this increases the risk of getting "mouse arm".
The way to use a mouse, is to rest your wrist on the desk, and move the mouse with your fingertips. None of these ergonomic ones allow you to do that. Instead, they force you to move your entire arm, increasing stress on the shoulder.
Someone should tell the mouse manufacturers that the problem isn't that the hand isn't resting "comfortably" around the mouse, but rather that the user moves and strains his shoulder.
It's worse, since there is absolutely no performance difference in prefix compared to postfix notation. Unless, of course, you completely disable optimisations. But if you do, then you have bigger performance issues to worry about.:-)
Yeah, but that would ALSO kill all the.NET development on Windows at the same time. There are tons of MS.NET developers now; MS wants them to use their tools. Non-discriminatory means they'd have to kill off their own fanboy dev armada in order to get at the Mono gnat.
Not if they include a license with every Windows license. That would be a very effective way of getting what they want.
My iPod is extremely scratched, on every side of it. However, I kinda like it that way. The worn look makes it look cool. I'm also very happy that I don't have to worry about getting it scratched.
Slashdot Mirror
My point is that a formal proving process is not necessarily better than an ad-hoc code verification process in the respect that just because you can (using a tool, which we for argument's sake can assume to be bug-free) prove that your program conforms to a formally written specification doesn't mean that the code will work. All you have proved is that it conforms to the specification. You simply moved the potential for bugs from the implementation to the formal specification. The problem is that the formal specification is just as or even more complicated to read and write than the implementation itself. Not to mention the fact that very few people know how to express software designs in a mathematical notation rather than code, and even fewer people a actually prefer that notation to normal computer code.
I think your last paragraph is the most correct one. The real benefit of the formal proving process is that it forces the reviewer to actually go through the code. There is no way to just gloss over the code.
At the end of the day you're going to end up with a hell of a lot more documentation and proofs that no one will ever read, and the system won't be much better than the system that wasn't proven.
Thanks to this, a lot of interesting stuff becomes possible, such as the fast file system creation which is demonstrated in this very cool demo.
If you don't consider ZFS a quantum leap in file system technology, I wonder what it would take for you to use that expression (set aside for the moment the people who argue that "wuantum leap" should in fact mean the opposite :-) ).
Imagine being able to take really fast working copies of whatever you're doing and be able to simple use the old versions by cd'ing to the old clone.
That's certainly what I would use ZFS for. The rest of the stuff, pooling and mirroring and stuff is less interesting in my laptop. :-)
Assuming a standard 19-inch rack which holds 96 drives, you'd need 256147 racks to hold the drives. Given a floor size of 0.16 square metres per rack, you'd end up with 3.779 football fields worth of racks.
I leave it to someone else to calculate the heat dissipation from this array.
I think you meant to say that whitespace indentation matters, in which case I agree with you.
I wonder why. In fact, I think this is a great idea. It gives the consumer a chioce. Either he won't care one bit about this "interactive" commercial and keep fast-forwarding through them or he can get involved and watch the commercial thoroughly, adding value for himself as well as the supplier of the ad.
This is the way a free market is supposed to work. If the consumer doesn't want to watch the commercials, add some value to them. No one is still not forcing you to watch the commercial.
I definitiely prefer this to some other sceme where the cable companies block the fast-forward button during the commericals like they do on DVD's.
In any case, this is one of the reasons why I stopped playing WoW after about a week.
You can't become good.
You can become experienced, you can invest a lot of time and thus get a higher experience level, you can build a large network of people to chat with... But you can't become a skilled WoW player.
Just about the only skill you can obtain is learning all the maps and the missions. The rest of the time is being spent doing the same thing over and over again in order to raise your XP. Even games that I utterly dislike, such as CS, allows you to become skilled. Actually, most glames do, but not the MMORPGs. I honestly don't understand why. Perhaps it's because most people are not prepared to practice something? Perhaps WoW is just an alternative to planting oneself in front of the TV, watching MTV? (i.e. no intelligence required). I don't know, and by now I don't really think I care.
Now that I'm writing a post about WoW, I have to add my pet peeve as wel:
Playing WoW, it feels like I'm trapped in the Twilight Zone. I walk around in a living world, things happen all around me, but no one can really see me. I'm like a walking shadow, somehow being able to touch things, but still not. Anything I do have absolutely zero effect on the world. It really kills the immersion for me when an NPC tells me that I need to save the village by killing this or that monster. I do it, I arrive in a triumphant return... but... No... Wait... Nothing changed! The village is apparently still held in the grasp of this monster, since the very same person is still handing out the same quest to other players. I'm still the same no-one I was before, altough with a couple of more experience points, and the world laughts in my face saying: "Don't think you can be someone special. You're always doomed to be a boring no-one, and you'll never affect the world".
I think that's the real problem with WoW.
No need to. Just wait around for it to be left at the nearest object.
The problem with fingerprints is that it's inherently a very insecure way of authentication for two reasons:
Firstly, you can't change it if it leaks out. A password or a credit card number can be easily changed and the damage minimised in case of an information leak. Doing this with a fingerprint is much harder.
Secondly, the fingerprint is very hard to keep secret. Your body has this annoying ability to leave copies of your identification token all over the place, very easy for anyone to pick up. If you were worried about the ability to scan proximity tags (RFID), then you should be really scared about the use of fingerprints as authentication tokens.
If you don't believe me how easy it is to pick up, read this about how to make a copy of ones fingerprint using common household items.
Anyway, even the good shows on public service radio mix their shows with yet more "hit" music making them rather painful to listen to. You're enjoying a fun comedy show and all of a sudden: Bang! You get hit over the head with Britney Spears.
Now, the good thing is that public service radio has started to make their shows available as podcasts. I download them via ITMS. Because of (or shall I say thanks to) the music agreemets, all the commercial music is edited out of the shows. I couldn't be happier. I finally get to listen to the show the way I want it and I don't even have to fast-forward. In this particular case, I hope they don't sign a music distribution agreement for the podcasts. Most of the people I've talked to about this agree as well.
If I really want the shows mixed with music, I can just switch to one of my other thousands of songs I already have on my iPod.
What I was trying to say was that Apple has nothing to gain by trying to push out Linux. If anything, they have a lot to lose if that were to happen.
First of all, Apple is actively competing against MS in a way that even surprises many Mac fanatics, for example by releasing Pages in addition to Keynote. Apple losing MS Office would not be very good for their business. While in a somewhat different segment, the media player competition between Apple and MS is also quite fierce.
Secondly, Linux does not pose any major threat against MS and Apple at this time. Granted, MS loses users to Linux but Apple is stealing Linux users to OSX. I fail to see what MS has to contribute here.
Another slight nitpick. The youngest dinosaur bones are 65 million years old. The oldest are areound 230 million years old.
There. Done. It's now written i C and C++. Download the source and take a look.
(yes, there is some Java in there, but you can run it perfectly without it)
What is going to be tested is the implementation, not the theory behind the algorithm, however. It doesn't really matter how well proven the algorithm is if the implementation has a bug (which could caused by a typo for example).
Code proving is a nice theoretical excersise, but don't for a second believe that just because some code has been put through a formal proof that it cannot contain bugs.
Most of them are big as houses are requires you to move your entire hand to move the damn thing around the desk. If anything, this increases the risk of getting "mouse arm".
The way to use a mouse, is to rest your wrist on the desk, and move the mouse with your fingertips. None of these ergonomic ones allow you to do that. Instead, they force you to move your entire arm, increasing stress on the shoulder.
Someone should tell the mouse manufacturers that the problem isn't that the hand isn't resting "comfortably" around the mouse, but rather that the user moves and strains his shoulder.
They could support any license they want. Let's just wait until we see anything significant released under that license.
You also fail to know mention what country your wife lived in. You do realise that she didn't stay in a country called "Africa" did you?
I'm sorry, but to me you seem to show the same kind of ignorance as you blame others to show.
I'm not even going into the details in trying to explain to you that there are huge differences between countries in Africa.
Embedded (virus) scripts
It's worse, since there is absolutely no performance difference in prefix compared to postfix notation. Unless, of course, you completely disable optimisations. But if you do, then you have bigger performance issues to worry about. :-)
Apparently you can get sued for singing with the kids
My iPod is extremely scratched, on every side of it. However, I kinda like it that way. The worn look makes it look cool. I'm also very happy that I don't have to worry about getting it scratched.