You should never prove programs the way CS instructors teach. If they knew - really knew - how to do it well, they'd be off making millions as consultants for designers of mission-critical projects. I've never seen a lecturer turn up in top-quality designer jackets eating caviar, so it is reasonable to assume they're either (a) vegan, or (b) not as knowledgable as they like to claim.
How would I solve the scalability problem? I wouldn't. One of the most important rules in maths is that if a problem is not easily solvable in one domain, you should transform it into one it can be easily solved in.
This applies to formal methods. A Z Specification, for example, describes a set of states and state changes. All problems need to be reduced to something in this format to be usable. When a problem cannot be trivially reduced, you apply transforms until it can.
For example, threading. You describe the thread as the state and the operations that the thread can do are the statements reflecting the state change. You would do a whole different set of schemas for the operations themselves. And then another set for every other dimension that you can identify.
You are correct that proving more than a few hundred lines is extremely hard, but if you assume "black box" development, you only ever have to prove the box. Nothing outside of the box matters, because it will have no impact on the inside.
It is time-consuming, it does require some very skilled mathematicians, but it can be translated into a set of problems where each member of the set is solvable.
We're not talking about fixing bugs, we're talking about ripping the specification out of the original software, fixing that specification so that it is 100% bug-free, then writing an entirely clean-room copy from that specification alone. A good design should produce damn-near no bugs.
Secondly, bugs only spread in the way you describe in unstructured code. If each module is strictly black-box, no bug can EVER spread outside of that box OR enter into it from the outside.
Thirdly, black-box coders don't talk to each other, so communication is a non-issue. Same with reverse-engineers. You have some block of code, you turn it into a specification, you then prove that the specification is correct and matches the code. Communication between individuals is irrelevent, because there is nothing that one is dealing with that will impact another. That's not the way this kind of engineering is done.
Because no communication is required, no communication problem exists. Remember, the logic of the unit is treated by one person and any given single interface or set of interfaces by another. Even the interface person doesn't need to talk to anyone. They know from the spec what the inputs and outputs are, they don't need to know or care what they do, only how they interconnect to each other or other black boxes, between contexts, processes or threads. ALL they have is the interface to study.
There is no debugging here and none of the usual team rules apply, because you'd have 10,000 independent teams of 1 person, not 1 team with 10,000 people.
The complaints raised by most other people show a woeful lack of imagination on how to apply formal methods. First rule of mathematics: If you can't solve the problem in one domain, apply a suitable transform and turn it into a domain you can solve the problem in.
However, your talk of debugging indicates the malady runs deeper and that there is also a woeful lack of understanding of what formal methods even are.
The timeframes are based on the assumption that the original code is essentially junk, that what you want to do is get the APIs, system calls and abstract behaviour from the original system. Once you have that information, you'd then clean up the specification (so it won't necessarily be the same as the original, but it is certain to work), and then and only then would you re-implement, totally from scratch.
The certification system would ideally be fine-grained and cover all kinds of behaviours, but consumers get confused easily. As such, it seems better to reward good practices such that the only way to stay ahead of the pack is for companies to keep improving those practices. The specifics of the bugs will then fall away of their own accord.
I used Z to help design some code for a high-power particle accelerator. I wouldn't personally call something like that a "mickey mouse" program - fifty gamma ray detectors, data processing nodes, data storage nodes, all interfaced to a user control system. So we're talking grid computing that needed exceptionally high reliability and an exceptionally good response time.
(In the end, those components of EUROGAM I was involved in writing were capable of handling 33 megabits/second - and it was the network that failed before my software. Those components included data storage, linear interpolation of matrices with any size dimensions and any number of dimensions, data display and data upload/download to external storage.)
Project scale doesn't matter, because good software design is all black-box. All contexts and all threads are logically independent except at controlled points, so you push all of the complexities a regular formal language cannot deal with into those controlled points and prove the rest as ordinary modules.
The controlled points then aren't any more complex. They are not really systems, the variation is between threads/contexts and not time, so you simply rotate the problem and write your Z schemas between threads/contexts, and not between operations. There are no operations, you're at a single point.
The reason formal methods are regarded as "difficult" has nothing to do with any actual difficulty and everything to do with the fact that the industry has no desire to pay more for the extra skills needed and get the product later, because for them speed is everything. First to market. First to this. First to that. Gotta have it last week, no matter how broken, not next week, no matter how superior.
You do not have to "prove the whole OS" - that is monolithic thinking. You only have to prove each black box (horizontal slices through the logic, if you like), each thread/state (vertical slices, using the same analogy), each interface and the entire initial state. By taking fragments of slice, you reduce any specific problem to one that can trivially be solved. By slicing in every direction and doing the same, you reduce ALL the problems into ones that are trivial to solve. By finally proving the interfaces between fragments of slice (whether the fragments are in the same slice or not), you prove that all micro-flows are valid.
Provided your proofs are satisfactory, you can now prove by induction any given horizontal or vertical slice in its entirity. Since we know the interactions between the two directions are valid (as that's already been proved), we can now prove by induction the full array of horizontal and vertical slices.
Honestly, the biggest problem I see to the adoption of widespread use of formal methods are the lecturers who introduce it but who completely lack the understanding necessary to apply what they are teaching. Remember, those who can do, those who can't teach. Don't trust those who can't as the source of wisdom.
My usual rule of thumb is to provide the PHB a list of all of the benefits they, personally, will get, any recognition they will receive, any speedups they will experience... To be a boss requires a high level of self-importance and ego, so you simply make sure that you feed these generously.
Have two machines and load-balance between them. That way, the "spare" isn't "wasting space" (as far as the PHB is concerned), when things are going well you get double the performance, you have no downtime switching servers when one fails, and because you're placing half the stress on each machine, you more than halve the risk of a failure.
If there had been a provably correct design from which the coders operated, OR if Microsoft had elected to spend the time reverse-engineering a design, then getting it into a provably correct form, then re-implemented Windows from that design.
You can create bullet-proof software in a totally proprietary fashion. The problem is that bullet-proof code requires far more designers and coders than most companies can throw at the problem. Open Source is good, from that perspective, in that a single company doesn't need to find huge armies of coders.
It would be possible to formally prove Fedora Core, and get it 99.99% bug-free, but Red Hat can't afford to hire the hundreds of thousands of brilliant engineers it would require. However, there probably ARE a few hundred thousand brilliant engineers who have access to the Internet who could perform a complete re-designing and re-implementation on the scale you'd need, who would be willing to volunteer at least a little time to do so.
I've shown elsewhere that this is not true of Microsoft, who really could afford to hire the extra staff needed to completely re-engineer Windows in a provably correct form that would also run at a decent speed. They don't have any of the usual excuses. They burn 6 billion a year on R&D they don't do anything useful with, they have offices in virtually every country so can draw directly on the manpower of every single one of those countries without any work authorization issues. And they could do it all without having to sacrifice their egos or a single line of source.
Theirs is not a fate caused by the limitations of human beings. Theirs is a fate entirely created and sustained by choice alone.
However, there are usually solutions. At least, to parts of the problem. The use of formal methods will mean that you can eliminate (almost) all bugs caused through design and makes it easier to validate code for bugs caused through implementation. Unless you also write the compiler (or have access to a formally-written compiler), it is much harder to validate that the binary is correct.
It was noted elsewhere that Microsoft spends six billion a year on R&D. If they hired mathematically-inclined software engineers at 100,000 a go, they'd be able to keep a small army of 10,000 such programmers. You can probably reverse-engineer a specification, prove, then re-engineer the code for about 10 lines an hour. Assuming a 40 hour week, that means they could formally re-engineer 208 million lines of Windows per year. Even with all of the standard applications, libraries and utilities, the team should have an iron-clad damn-near-bugproof Windows within 2-3 years. It wouldn't cost them any more than they're already burning on patents for stuff nobody else cares about, and would save three times the total cost of the bugs to the country within a single year.
The overflows are easier. You compile all the applications with something like ElectricFence, dmalloc, or some other debugging malloc. A few tests at Microsoft should then collect a lot of the overflows. You then recompile such that the debugs won't cause fatal errors but will still generate alerts. You have the Windows error reporting tool collect all those alerts and either notify the user at the time & allow them to send, or send in bulk on the next major error. Microsoft can then fix the overflows BEFORE someone exploits them, because the odds are high that they'll be accidentally triggered long before any black hat learns about them. If only because there are several hundred million users, and most will be trying to do things that are impossible or - at the very least - seriously warped.
Of course, they could also get a copy of the Stanford Code Validator, or even just download a copy of splint off the Internet. Both would pick up the majority of coding errors and allow Microsoft to fix them.
Regardless of which of these solutions is used, a company the size of Microsoft should be able to completely and utterly clean their software of 98%-99% of its defects within three to four years. As the article noted, it has now been over four years since the proclamation of taking security seriously, but yet there is no sign of any kind of rigorous campaign to really erradicate faults. Rather, there seems to be much more of a campaign to make users more accepting of the fact that there are faults.
Not everyone can guarantee 99% fault-free software within a reasonable timeframe. There aren't the mathematician/software engineers, for a start. However, maybe it would be possible to have a standards authority that could certify a software product as "mid-grade" (50% bug-free), "high-grade" (75% bug-free) or "mission-critical" (99.99% bug-free). Software providers could elect whether or not to be certified and consumers would then be free to decide how much quality they want to pay for, because they'd know how much quality was there. Consumers would also be in a stronger position to interpret the lack of such certification.
Welcome to this meeting of IPaholics Anonymous, where people share their experience, strength and hope in their battle against their addiction to Intellectual Property lawsuits. Here are the twelve steps, adapted from other recovery programs.
We admitted we were powerless against Open Source initiatives, that our contempt for common folk and peasents had become unmanageable.
We came to believe that a sharing methodology greater than ourselves could restors us to sanity.
Made a decision to turn our will, lives and FTP address to Freshmeat, as we understand Freshmeat.
Made a searching and moral inventory of what sourcecode we actually have and own.
Admitted to ourselves, Slashdot and Richard Stallman the exact nature of our licensing errors.
Were entirely ready to let the OSI and the FSF remove these defects of proprietaryness.
Humbly asked/dev/null to remove our closed licensing agreements.
Made a list of all people we'd totally ripped off and became willing to send upgrades to them all.
Directly sent their IT departments the necessary patches, except when to do so would break something else.
Continued to grep license files and when they were closed, promply GPL them.
Sought through LinuxFest and Slashdot to improve our concious contact with the F/LOSS meme as we understood F/LOSS, asking only for Linus Torvald's will and the processing power to carry that out.
Having had a sourcecode awakening as a result of these steps, we tried to carry this message to compulsive proprietary coders and to practice good coding in all our affairs.
I would say that I spend in excess of 50% of the day, each day, every day, in front of the computer. I'd also say that I've done very nearly that for the past 27 years. My vision has shown no real deterioration in that time.
HOWEVER, I would point out a few things here. First, I set the refresh rate to something my eyes are comfortable with. Too low a refresh rate will likely cause headaches and eye-strain, though I doubt it can actually harm your vision.
Secondly, I've generally used monitors that are either anti-glare or fitted with anti-glare screens. Reflections off the monitor will also cause eye-strain. For the same reason, monitors should not be positioned to reflect inside lights or the outside.
Thirdly, adjust the contrast and brightness sensibly. In general, I've found it best to use the minimum brightness and then raise the contrast until the picture is comfortable on the eyes.
Lastly, the best computer wallpaper seems to be soft colours with motion, as you're mentally going to be placing that in the background of whatever you're focussed on.
That is interesting. I can definitely see it. I'd worry if a person tried pumping 150 KV through their computer, just to even out the temperature, though.
Lightning can be detected with any radio or even a magnetic compass. (In fact, the effect on electrical and magnetic systems played a big part in the invention of the radio.)
Now, if you were to suggest that nobody looked before, I'd find that all too believable. It is truly amazing how much gets "discovered" very late on, because of poor observations and hyper-cynicism. (The plasmas that rise up above some storm clouds, when there is lightning, were "known about" a LONG time before they were officially "discovered", and have likely existed long before there was life capable of observing them. Skeptisism is important, but you can't be so skeptical that you won't look and so cynical that you won't listen. You'll never see much if you keep your eyes closed.)
Is hyper-cynicism possible here? Sure. Thunder isn't predicted by the standard model, so it is unlikely anybody would have gone looking and it's doubtful anyone who has observed lightning in a hurricane would have been believed. That's not to say that's what's happened - it could well be that this really is a staggeringly rare phenomina - but it's entirely believable that it did.
The observation planes may or may not have seen lightning (depends on where in the storm mass it occurs), but they should have heard it on the radio and seen it on the aircraft's magnetic compass. The clicks caused by lightning are trivial to identify, even if the lightning itself was completely obscured. Radio Hams should also have heard the distinct sounds of approaching lightning. If any of these people kept recordings (unlikely, but possible) then it would be fairly trivial work to go through those and determine just how common lightning in a hurricane is.
Now to convince NASA to not just be humble, but to actually do this kind of research that could really already have been done.
Well, almost. I was 8 at the time I got my hands on a PET 3032. The sound trick was one I learned from one of the guys at Oxford Computer Systems, who sold the PETSpeed compiler. (Somewhere, I still have the sticky labels and demo pack, though I seem to remember doing VERY nasty things to the Dragon BASIC compiler, which was utter carp.) They had some demo sounds on their computer, but the proof of the pudding was getting the full, glorious sound effects from Commodore's space invaders.
The VICE emulator supports the sound system and documents how it worked, though, so you can still re-create those bygone days.
You can do perfectly good single-channel music on the PET, by cycling the status pin on the serial port, then placing a radio near it. You could also use the SoundBox, which IIRC plugged into the serial port, but it really came to the same thing.
There was one experiment covered on Slashdot a looong time ago in which the person used mineral oil. Full emersion cooling has a major problem in that it would be easy to get backwaters in which there is little or no circulation. Air bubbles can also be a headache, for a similar reason.
You've got to watch the thermal range, if you're wanting to do extreme cooling OR run really hot hardware. Some of 3M's synthetic liquids are excellent for this type of project - well, they would be but only a handful of enthusiasts have ever been able to afford them.
Finally, although you only need to extract the amount of heat being put into a total emersion system, you've got to cycle through most/all of the liquid in a reasonably short period of time. You shouldn't rely on the heat simply transferring through the liquid. Besides, if you do that, some regions will be hotter than you'd like and others colder, even if the average is just fine. The average doesn't matter, because no component will see the average.
I thought John Nash had pretty well debunked most of Adam Smith's theories, so even if they were pro-AS, they're pro an idea that has been discredited anyway.
Oh, those were the days. I watched this really dull live demo of Prestel that was being given on the BBC's "Micro Live" computer show. Well, apparently someone else thought it was dull too. A person going by the handle of "Cheshire Catalyst" piped a really nice poem to the studio's console. Being live, there wasn't a whole lot anybody could do about it, either.
Live shows in general were always coming up with "oops" moments. Another classic was a semi-live action series called "The Avengers", which (at that time) starred Patrick McNee and Honor Blackman. In order to make the fight scenes realistic, they trained Ms. Blackman in actual martial arts to quite a high standard. This had one drawback. She was actually a good deal better at fighting than the stuntmen were at getting out of the way. More than one ended up unconcious in the studio, but with no ability to edit the recordings, they just had to stay there until they cut to a different scene.
Databases are interesting, in that files tend to creep in size and only occasionally packed down. These are read/write operations, only initial setup will involve any creates, and there are probably no destroys at all. Files will not be looked for, and the file datestamp is unimportant.
The closest parallel to most of these operations is in the copying of a tarball, and then TARring up the Linux kernel. (Untarring creates files, and as I've said, creating files is not the bulk of a database's work.)
JFS does best, according to these benchmarks, with ext2/ext3 following close behind. The other filesystems aren't worth a damn for database work.
If you're a programmer using a distributed project manager, then creating large numbers of directories (but not removing them) is quite likely going to be a significant operation. For the same reason, computers acting as FTP mirrors will find that an important statistic.
PERL CPAN users will likely also be familiar with the notion of massive numbers of directories being created. Programs that create workspaces in the/tmp directory, on the assumption that the system will clean it up later, are also part of the create-only plague.
So if you are in any of these categories, ext2/ext3 should NOT be used for your workspace partition or the partition on which the/tmp directory resides.
There will be other cases, but those are the clearest to me.
No, I'd argue that the reason most people use ext2 and ext3 is that these are the filesystems that you get to use when you install the system. It's like arguing that most people use Windows because it's better - no, it's because it's there.
Secondly, you don't need to give every option to everyone. Red Hat's installer already lets you pick whether you're installing on a desktop, a server, or a custom system - so that automatically tells you which filing systems are likely to be wanted.
(eg: If you are installing for a desktop, you don't - probably - want a filing system geared for high-end servers. Likewise, a server box won't want a desktop-optimized filesystem. Custom installs should be exactly that, allowing you to custom-pick whatever you damn well like for the filesystem.)
So, uh, fedora developers are stupid and you're smarter than them?
That's easy. Yes.
The entire release cycle methodology is flawed (development needs to be split into alpha and beta, where alpha is the latest release and beta is the set of RPMs that will co-habit the hard drive. When RPMs are built, a complete dependency map should be constructed and compiled.
Since "development" basically means "it'll compile, but it's not tested", you could cross-compile development trees for EVERY architecture Linux supports, on the grounds that you don't give a damn if unsupported binaries will actually run, but if they do, you've increased interest in that distribution and are in a position to expand and support other architectures if the interest turns out to be there. Costs nothing, but potentially earns lots.
It is obnoxiously difficult to get 3rd party RPMs into even the extras branch. Many programs have multiple configurations possible, but are often compiled with random, unexplained ones that make no obvious sense. RPMs that are present are sometimes ancient (HDF5 is at 1.6.5 with no szip support, in the extras, but the current version is 1.7.52 and szip is at 2.0. ATLAS - a very important maths library - is at 3.6.0, but the current "recommended" release is 3.7.11! The version of LAM is ancient and should be replaced with OpenMPI anyway.)
Yes, I would regard the Fedora developers as too slow, too entrenched and not interested in producing the optimal distribution, only the best one they can produce at minimal effort. To me, that is wholly unacceptable. Towards the end of the last ice age, you could understand people conserving effort. That is no longer the most efficient way to get things done.
(If anyone out there cares to provide some disk space, I'd be more than happy to show how Red Hat could be done better, with greater versatility, yet with fewer headaches for the novices.)
Europeans can reasonably expect other Europeans to help safeguard their privacy. Part of that is mutual interest, part is a reasonably comprehensive network of privacy laws that consumers (and governments) can use to skewer anyone who transgresses (and is discovered). Although territorial claims aren't particularly protected in, say, Britain (it still has no law of trespass), personal privacy is generally very well protected.
Now, if quaint, olde worlde countries like Britain can succeed in offering a high level of information privacy, then modern, advanced, sophisticated countries like the United States should have exactly the same ability.
If the population in said olde worlde country can produce a well-known figure like the comedian Steven Fry and yet have such a major celebrity able to simply "vanish" for weeks on end, so that he could spend time chilling out without the usual pressure from the press...
If the population can even produce a mysterious piano-playing genius - discovered much later to have been from East Germany - despite every effort by police, the medical profession, the entire British media, etc, to be the first to get a name and place of origin... (Despite the glare of attention, it took over two months for the mystery to be solved.)
If you start by knowing all of that, AND you know that the information being traded in the States is just a bunch of statistics that have no actual meaning anyway, then why CAN'T we expect the US to follow suit, with strong privacy laws from above and strong privacy respect from the grassroots?
From a brief examination of the benchmarks, I'd say the following would seem to hold up:
JFS: Great for software development, as it allows rapid file and directory reads, writes, creates and deletes
XFS: Seems to work best with much more stable content. Creating and mounting the partition is also fast, and the FS overhead seemed low. Should be good for static databases, particularly if you're going to use a network filing system to access the drive, say using a SAN.
Reiser4: Surprisingly, I didn't see Reiser4 really shine at a whole lot in the benchmarks. The massive mount time tells me it needs to be a local drive that only needs mounting the once. Just not sure what sort of data would be best on it.
Ext2/Ext3: Mediocre at almost everything. Distros like Fedora that mandate the initial install ONLY use Ext3 are being stupid. The best fall-back filing systems if you can't find anything better for what you want the partition to do, but should never be used in specialized contexts.
Doubling the number of coders will double the number of bugs and double the total time
Doubling the budget will double the number of coders
Extendable projects will, deadlines kill
There is no such thing as a potential bug
"Good" methods are cheap for customers, sloppy methods are profitable for companies.
In the end, software companies are in it for the profits. They have no lemon laws to respect, they have no trades description act to obey, no ombudsmen to answer to, no consumer rights groups to speak of, no Government-imposed standards certification and virtually no significant competition. Customers are often infinitely patient and completely ignorant of what they should be getting - the machines are like Gods and the software salesmen are their High Priests. To question is to be smote.
Were standards to be mandated - perhaps formal methods for design, OR quality certification of the end result, you would see no real impact on net software costs. Starting costs would go up, but long-term costs would go down.
Nor would you see any serious impact on variety - if anything, there is a greater range of car manufacturer and design today than there was in the 50s and 60s when cars had the unnerving habit of exploding for no apparent reason.
What you'd see is a decline in stupid bugs, a decline in bloat, an increase in modularity, possibly a reduction in latency and a move from upgrades to fix things that SHOULD have worked in the first place to enhancing things that can be relied upon to CONTINUE working fter the patches.
Money would not be made by selling the same product with a different set of defects to the same market, money would be made by always going beyond last year's horizons. The same way most manufacturers, from cars to camping gear to remote control aircraft to air conditioning units to microwave ovens to home stereo manufacturers have all been doing - very successfully - for a very long time.
The IT industry isn't going to change in the foreseeable future, the only way we'll see change in our lifetimes is if it is imposed on the Pointy Haired Bosses. We could easily see 99.9% reliable software, with no additional cost, in our homes in a year, with the lack of constant fixes actually saving money. And that's why it won't happen. Not because the IT corporations are mean, thuggish and ogreish - they are, it just isn't way it won't happen.
It won't happen because they're geared both towards the profit motive and towards the outdated notion that the market is tiny. (That last part was true - in the 1950s, when entire countries might have three or four computers in total, operating in two, maybe three different capacities. You can understand a desire to go after the after-sales service, when there simply isn't anything else left to do.)
Today, Microsoft's Windows resides on 98% of the desktop computers, but because of the support system needed to run the damn things, 98% of the world's population didn't have significant access to one. Ok, putrid green is a lousy colour, but the idea of clockwork near-indestructible laptops that - in theory - could be built to weigh 5 lbs or less and run high-end, intensive applications is beginning to filter through to the brain-dead we call politicians.
You think someone in the middle of Ethiopia who is fluent only in their native tounge is going to want to pay for telephone technical support from someone in India, in order to figure out why their machine keeps locking up?
When computing is truly available to the masses (ie: when even a long-forgotten South American tribe can reasonably gain access to one), the ONLY way it can be remotely practical is if said South American can look forward to a reliable, usable, practical experience where all usage can be inferred from first principles, and where NO software service calls are required to get things to work, ONLY required to get more things for working with.
Slashdot Mirror
How would I solve the scalability problem? I wouldn't. One of the most important rules in maths is that if a problem is not easily solvable in one domain, you should transform it into one it can be easily solved in.
This applies to formal methods. A Z Specification, for example, describes a set of states and state changes. All problems need to be reduced to something in this format to be usable. When a problem cannot be trivially reduced, you apply transforms until it can.
For example, threading. You describe the thread as the state and the operations that the thread can do are the statements reflecting the state change. You would do a whole different set of schemas for the operations themselves. And then another set for every other dimension that you can identify.
You are correct that proving more than a few hundred lines is extremely hard, but if you assume "black box" development, you only ever have to prove the box. Nothing outside of the box matters, because it will have no impact on the inside.
It is time-consuming, it does require some very skilled mathematicians, but it can be translated into a set of problems where each member of the set is solvable.
Secondly, bugs only spread in the way you describe in unstructured code. If each module is strictly black-box, no bug can EVER spread outside of that box OR enter into it from the outside.
Thirdly, black-box coders don't talk to each other, so communication is a non-issue. Same with reverse-engineers. You have some block of code, you turn it into a specification, you then prove that the specification is correct and matches the code. Communication between individuals is irrelevent, because there is nothing that one is dealing with that will impact another. That's not the way this kind of engineering is done.
Because no communication is required, no communication problem exists. Remember, the logic of the unit is treated by one person and any given single interface or set of interfaces by another. Even the interface person doesn't need to talk to anyone. They know from the spec what the inputs and outputs are, they don't need to know or care what they do, only how they interconnect to each other or other black boxes, between contexts, processes or threads. ALL they have is the interface to study.
There is no debugging here and none of the usual team rules apply, because you'd have 10,000 independent teams of 1 person, not 1 team with 10,000 people.
The complaints raised by most other people show a woeful lack of imagination on how to apply formal methods. First rule of mathematics: If you can't solve the problem in one domain, apply a suitable transform and turn it into a domain you can solve the problem in.
However, your talk of debugging indicates the malady runs deeper and that there is also a woeful lack of understanding of what formal methods even are.
The certification system would ideally be fine-grained and cover all kinds of behaviours, but consumers get confused easily. As such, it seems better to reward good practices such that the only way to stay ahead of the pack is for companies to keep improving those practices. The specifics of the bugs will then fall away of their own accord.
(In the end, those components of EUROGAM I was involved in writing were capable of handling 33 megabits/second - and it was the network that failed before my software. Those components included data storage, linear interpolation of matrices with any size dimensions and any number of dimensions, data display and data upload/download to external storage.)
Project scale doesn't matter, because good software design is all black-box. All contexts and all threads are logically independent except at controlled points, so you push all of the complexities a regular formal language cannot deal with into those controlled points and prove the rest as ordinary modules.
The controlled points then aren't any more complex. They are not really systems, the variation is between threads/contexts and not time, so you simply rotate the problem and write your Z schemas between threads/contexts, and not between operations. There are no operations, you're at a single point.
The reason formal methods are regarded as "difficult" has nothing to do with any actual difficulty and everything to do with the fact that the industry has no desire to pay more for the extra skills needed and get the product later, because for them speed is everything. First to market. First to this. First to that. Gotta have it last week, no matter how broken, not next week, no matter how superior.
You do not have to "prove the whole OS" - that is monolithic thinking. You only have to prove each black box (horizontal slices through the logic, if you like), each thread/state (vertical slices, using the same analogy), each interface and the entire initial state. By taking fragments of slice, you reduce any specific problem to one that can trivially be solved. By slicing in every direction and doing the same, you reduce ALL the problems into ones that are trivial to solve. By finally proving the interfaces between fragments of slice (whether the fragments are in the same slice or not), you prove that all micro-flows are valid.
Provided your proofs are satisfactory, you can now prove by induction any given horizontal or vertical slice in its entirity. Since we know the interactions between the two directions are valid (as that's already been proved), we can now prove by induction the full array of horizontal and vertical slices.
Honestly, the biggest problem I see to the adoption of widespread use of formal methods are the lecturers who introduce it but who completely lack the understanding necessary to apply what they are teaching. Remember, those who can do, those who can't teach. Don't trust those who can't as the source of wisdom.
My usual rule of thumb is to provide the PHB a list of all of the benefits they, personally, will get, any recognition they will receive, any speedups they will experience... To be a boss requires a high level of self-importance and ego, so you simply make sure that you feed these generously.
Have two machines and load-balance between them. That way, the "spare" isn't "wasting space" (as far as the PHB is concerned), when things are going well you get double the performance, you have no downtime switching servers when one fails, and because you're placing half the stress on each machine, you more than halve the risk of a failure.
You can create bullet-proof software in a totally proprietary fashion. The problem is that bullet-proof code requires far more designers and coders than most companies can throw at the problem. Open Source is good, from that perspective, in that a single company doesn't need to find huge armies of coders.
It would be possible to formally prove Fedora Core, and get it 99.99% bug-free, but Red Hat can't afford to hire the hundreds of thousands of brilliant engineers it would require. However, there probably ARE a few hundred thousand brilliant engineers who have access to the Internet who could perform a complete re-designing and re-implementation on the scale you'd need, who would be willing to volunteer at least a little time to do so.
I've shown elsewhere that this is not true of Microsoft, who really could afford to hire the extra staff needed to completely re-engineer Windows in a provably correct form that would also run at a decent speed. They don't have any of the usual excuses. They burn 6 billion a year on R&D they don't do anything useful with, they have offices in virtually every country so can draw directly on the manpower of every single one of those countries without any work authorization issues. And they could do it all without having to sacrifice their egos or a single line of source.
Theirs is not a fate caused by the limitations of human beings. Theirs is a fate entirely created and sustained by choice alone.
It was noted elsewhere that Microsoft spends six billion a year on R&D. If they hired mathematically-inclined software engineers at 100,000 a go, they'd be able to keep a small army of 10,000 such programmers. You can probably reverse-engineer a specification, prove, then re-engineer the code for about 10 lines an hour. Assuming a 40 hour week, that means they could formally re-engineer 208 million lines of Windows per year. Even with all of the standard applications, libraries and utilities, the team should have an iron-clad damn-near-bugproof Windows within 2-3 years. It wouldn't cost them any more than they're already burning on patents for stuff nobody else cares about, and would save three times the total cost of the bugs to the country within a single year.
The overflows are easier. You compile all the applications with something like ElectricFence, dmalloc, or some other debugging malloc. A few tests at Microsoft should then collect a lot of the overflows. You then recompile such that the debugs won't cause fatal errors but will still generate alerts. You have the Windows error reporting tool collect all those alerts and either notify the user at the time & allow them to send, or send in bulk on the next major error. Microsoft can then fix the overflows BEFORE someone exploits them, because the odds are high that they'll be accidentally triggered long before any black hat learns about them. If only because there are several hundred million users, and most will be trying to do things that are impossible or - at the very least - seriously warped.
Of course, they could also get a copy of the Stanford Code Validator, or even just download a copy of splint off the Internet. Both would pick up the majority of coding errors and allow Microsoft to fix them.
Regardless of which of these solutions is used, a company the size of Microsoft should be able to completely and utterly clean their software of 98%-99% of its defects within three to four years. As the article noted, it has now been over four years since the proclamation of taking security seriously, but yet there is no sign of any kind of rigorous campaign to really erradicate faults. Rather, there seems to be much more of a campaign to make users more accepting of the fact that there are faults.
Not everyone can guarantee 99% fault-free software within a reasonable timeframe. There aren't the mathematician/software engineers, for a start. However, maybe it would be possible to have a standards authority that could certify a software product as "mid-grade" (50% bug-free), "high-grade" (75% bug-free) or "mission-critical" (99.99% bug-free). Software providers could elect whether or not to be certified and consumers would then be free to decide how much quality they want to pay for, because they'd know how much quality was there. Consumers would also be in a stronger position to interpret the lack of such certification.
Thoughts?
HOWEVER, I would point out a few things here. First, I set the refresh rate to something my eyes are comfortable with. Too low a refresh rate will likely cause headaches and eye-strain, though I doubt it can actually harm your vision.
Secondly, I've generally used monitors that are either anti-glare or fitted with anti-glare screens. Reflections off the monitor will also cause eye-strain. For the same reason, monitors should not be positioned to reflect inside lights or the outside.
Thirdly, adjust the contrast and brightness sensibly. In general, I've found it best to use the minimum brightness and then raise the contrast until the picture is comfortable on the eyes.
Lastly, the best computer wallpaper seems to be soft colours with motion, as you're mentally going to be placing that in the background of whatever you're focussed on.
That is interesting. I can definitely see it. I'd worry if a person tried pumping 150 KV through their computer, just to even out the temperature, though.
...it was pronounced D flat.
Now, if you were to suggest that nobody looked before, I'd find that all too believable. It is truly amazing how much gets "discovered" very late on, because of poor observations and hyper-cynicism. (The plasmas that rise up above some storm clouds, when there is lightning, were "known about" a LONG time before they were officially "discovered", and have likely existed long before there was life capable of observing them. Skeptisism is important, but you can't be so skeptical that you won't look and so cynical that you won't listen. You'll never see much if you keep your eyes closed.)
Is hyper-cynicism possible here? Sure. Thunder isn't predicted by the standard model, so it is unlikely anybody would have gone looking and it's doubtful anyone who has observed lightning in a hurricane would have been believed. That's not to say that's what's happened - it could well be that this really is a staggeringly rare phenomina - but it's entirely believable that it did.
The observation planes may or may not have seen lightning (depends on where in the storm mass it occurs), but they should have heard it on the radio and seen it on the aircraft's magnetic compass. The clicks caused by lightning are trivial to identify, even if the lightning itself was completely obscured. Radio Hams should also have heard the distinct sounds of approaching lightning. If any of these people kept recordings (unlikely, but possible) then it would be fairly trivial work to go through those and determine just how common lightning in a hurricane is.
Now to convince NASA to not just be humble, but to actually do this kind of research that could really already have been done.
The VICE emulator supports the sound system and documents how it worked, though, so you can still re-create those bygone days.
You can do perfectly good single-channel music on the PET, by cycling the status pin on the serial port, then placing a radio near it. You could also use the SoundBox, which IIRC plugged into the serial port, but it really came to the same thing.
The RAM will be volatile and the ROMs are burned...
You've got to watch the thermal range, if you're wanting to do extreme cooling OR run really hot hardware. Some of 3M's synthetic liquids are excellent for this type of project - well, they would be but only a handful of enthusiasts have ever been able to afford them.
Finally, although you only need to extract the amount of heat being put into a total emersion system, you've got to cycle through most/all of the liquid in a reasonably short period of time. You shouldn't rely on the heat simply transferring through the liquid. Besides, if you do that, some regions will be hotter than you'd like and others colder, even if the average is just fine. The average doesn't matter, because no component will see the average.
I thought John Nash had pretty well debunked most of Adam Smith's theories, so even if they were pro-AS, they're pro an idea that has been discredited anyway.
Live shows in general were always coming up with "oops" moments. Another classic was a semi-live action series called "The Avengers", which (at that time) starred Patrick McNee and Honor Blackman. In order to make the fight scenes realistic, they trained Ms. Blackman in actual martial arts to quite a high standard. This had one drawback. She was actually a good deal better at fighting than the stuntmen were at getting out of the way. More than one ended up unconcious in the studio, but with no ability to edit the recordings, they just had to stay there until they cut to a different scene.
The closest parallel to most of these operations is in the copying of a tarball, and then TARring up the Linux kernel. (Untarring creates files, and as I've said, creating files is not the bulk of a database's work.)
JFS does best, according to these benchmarks, with ext2/ext3 following close behind. The other filesystems aren't worth a damn for database work.
PERL CPAN users will likely also be familiar with the notion of massive numbers of directories being created. Programs that create workspaces in the
So if you are in any of these categories, ext2/ext3 should NOT be used for your workspace partition or the partition on which the
There will be other cases, but those are the clearest to me.
Secondly, you don't need to give every option to everyone. Red Hat's installer already lets you pick whether you're installing on a desktop, a server, or a custom system - so that automatically tells you which filing systems are likely to be wanted.
(eg: If you are installing for a desktop, you don't - probably - want a filing system geared for high-end servers. Likewise, a server box won't want a desktop-optimized filesystem. Custom installs should be exactly that, allowing you to custom-pick whatever you damn well like for the filesystem.)
So, uh, fedora developers are stupid and you're smarter than them?
That's easy. Yes.
The entire release cycle methodology is flawed (development needs to be split into alpha and beta, where alpha is the latest release and beta is the set of RPMs that will co-habit the hard drive. When RPMs are built, a complete dependency map should be constructed and compiled.
Since "development" basically means "it'll compile, but it's not tested", you could cross-compile development trees for EVERY architecture Linux supports, on the grounds that you don't give a damn if unsupported binaries will actually run, but if they do, you've increased interest in that distribution and are in a position to expand and support other architectures if the interest turns out to be there. Costs nothing, but potentially earns lots.
It is obnoxiously difficult to get 3rd party RPMs into even the extras branch. Many programs have multiple configurations possible, but are often compiled with random, unexplained ones that make no obvious sense. RPMs that are present are sometimes ancient (HDF5 is at 1.6.5 with no szip support, in the extras, but the current version is 1.7.52 and szip is at 2.0. ATLAS - a very important maths library - is at 3.6.0, but the current "recommended" release is 3.7.11! The version of LAM is ancient and should be replaced with OpenMPI anyway.)
Yes, I would regard the Fedora developers as too slow, too entrenched and not interested in producing the optimal distribution, only the best one they can produce at minimal effort. To me, that is wholly unacceptable. Towards the end of the last ice age, you could understand people conserving effort. That is no longer the most efficient way to get things done.
(If anyone out there cares to provide some disk space, I'd be more than happy to show how Red Hat could be done better, with greater versatility, yet with fewer headaches for the novices.)
Now, if quaint, olde worlde countries like Britain can succeed in offering a high level of information privacy, then modern, advanced, sophisticated countries like the United States should have exactly the same ability.
If the population in said olde worlde country can produce a well-known figure like the comedian Steven Fry and yet have such a major celebrity able to simply "vanish" for weeks on end, so that he could spend time chilling out without the usual pressure from the press...
If the population can even produce a mysterious piano-playing genius - discovered much later to have been from East Germany - despite every effort by police, the medical profession, the entire British media, etc, to be the first to get a name and place of origin... (Despite the glare of attention, it took over two months for the mystery to be solved.)
If you start by knowing all of that, AND you know that the information being traded in the States is just a bunch of statistics that have no actual meaning anyway, then why CAN'T we expect the US to follow suit, with strong privacy laws from above and strong privacy respect from the grassroots?
In the end, software companies are in it for the profits. They have no lemon laws to respect, they have no trades description act to obey, no ombudsmen to answer to, no consumer rights groups to speak of, no Government-imposed standards certification and virtually no significant competition. Customers are often infinitely patient and completely ignorant of what they should be getting - the machines are like Gods and the software salesmen are their High Priests. To question is to be smote.
Were standards to be mandated - perhaps formal methods for design, OR quality certification of the end result, you would see no real impact on net software costs. Starting costs would go up, but long-term costs would go down.
Nor would you see any serious impact on variety - if anything, there is a greater range of car manufacturer and design today than there was in the 50s and 60s when cars had the unnerving habit of exploding for no apparent reason.
What you'd see is a decline in stupid bugs, a decline in bloat, an increase in modularity, possibly a reduction in latency and a move from upgrades to fix things that SHOULD have worked in the first place to enhancing things that can be relied upon to CONTINUE working fter the patches.
Money would not be made by selling the same product with a different set of defects to the same market, money would be made by always going beyond last year's horizons. The same way most manufacturers, from cars to camping gear to remote control aircraft to air conditioning units to microwave ovens to home stereo manufacturers have all been doing - very successfully - for a very long time.
The IT industry isn't going to change in the foreseeable future, the only way we'll see change in our lifetimes is if it is imposed on the Pointy Haired Bosses. We could easily see 99.9% reliable software, with no additional cost, in our homes in a year, with the lack of constant fixes actually saving money. And that's why it won't happen. Not because the IT corporations are mean, thuggish and ogreish - they are, it just isn't way it won't happen.
It won't happen because they're geared both towards the profit motive and towards the outdated notion that the market is tiny. (That last part was true - in the 1950s, when entire countries might have three or four computers in total, operating in two, maybe three different capacities. You can understand a desire to go after the after-sales service, when there simply isn't anything else left to do.)
Today, Microsoft's Windows resides on 98% of the desktop computers, but because of the support system needed to run the damn things, 98% of the world's population didn't have significant access to one. Ok, putrid green is a lousy colour, but the idea of clockwork near-indestructible laptops that - in theory - could be built to weigh 5 lbs or less and run high-end, intensive applications is beginning to filter through to the brain-dead we call politicians.
You think someone in the middle of Ethiopia who is fluent only in their native tounge is going to want to pay for telephone technical support from someone in India, in order to figure out why their machine keeps locking up?
When computing is truly available to the masses (ie: when even a long-forgotten South American tribe can reasonably gain access to one), the ONLY way it can be remotely practical is if said South American can look forward to a reliable, usable, practical experience where all usage can be inferred from first principles, and where NO software service calls are required to get things to work, ONLY required to get more things for working with.