This isn't about "process". Process won't guarantee anything except that you followed all the steps - it says nothing about what the quality of the end result will be.
Does application of formal methods guarantee zero defects? Of course not. Name any engineering discipline that can guarantee zero defects. There aren't any. As you yourself pointed out, even bridges fall down sometimes. However, I don't think an order of magnitude reduction in defect rates should be ignored. God knows, as a customer, I'd like to see software that doesn't break regulary.
With regard to program scheduling, while I don't think that formal methods are a panacaea, allow me to suggest that if you have no idea what you are doing it is hard to develop a schedule to do it. Doing some mathematical modeling beforehand allows you to gauge the size of the problem. This is how it's done in other engineering disciplines that involve the development of bespoke systems (my own experience in this case is with spacecraft design).
Yes, formal software methods are hard and time consuming compared to just building and testing.
That's not necessarily true:
I suppose that formal methods are arguably "harder", if by harder you mean "the developer actually has to understand what they are doing". But writing a program is writing a formal specification of what you want the computer to do. The formal methods crowd just advocate writing one or more specifications at a more abstract level as well, preferably in a notation that is amenable either to logical reasoning or mechanical state exploration (or both). The abstract specifications can be considered "prototypes" of the eventual system, that allow one to iron out assumptions and get the overall logic of the software right before you implement all the little details. Which is not to say that you won't revise your abstarct specs later based on things learned during coding - but having multiple layers of abstraction makes it easier to manager the conceptual complexity of the design process. It's really no different than building a bunch of UML models - except that formal models can actually be analyzed, while UML models rely on intuition an visual inspection to verify correctness.
There's good empirical evidence that formal methods do not actually take any longer than informal methods. Time spent developing formal models is gained back in a shorter test and debug cycle. There are many projects that have used formal methods such as Z or B to produce complex software in the same (or less) time as an equivalent project that does not use formal modeling. Those projects have typically also produced significantly lower defect rates in their delivered software. IBM reported a 9% cost reduction on the CICS project, and a much lower defect rate (although I don't have numbers). Praxis Critical Systems reports reductions in defect rate of up to an order of magnitude (depending on the system) with no increase in cost (see for example the UK CAA's CDIS system, or the Multos Certification Authority).
Are formal methods a silver bullet or panacaea? No. Do formal methods completely eliminate defects? No. But they can reduce their occurrence significantly. Do formal methods take longer? No. Do they cost more? No. In fact they can often result in cost savings. Are formal methods "harder"? Not really. Why aren't they used more? Because most software "engineers" are scared of learning the (actually relatively straightforward) math involved - it might take the fun out of software development! They'd much rather continue to perpetrate random acts of hackery in the hopes software that passes its unit-tests will continue to function as expected when applied to inputs that fall outside the range of test-cases they have tried.
And it will continue to happen until certain individuals realize that software is just as complex, if not more so than an engine. You don't slap one together and shove it in a car for consumers without giving it a solid saftey test. Software should be exactly the same.
You're right! Software should be exactly the same!
So why do software "engineers" not use the software analog of the finite element analysis, thermal modeling, combustion analysis, fluid dynamics, and other mathematical modeling that goes into engine design? That's what the grandparent meant by formal methods, not the idiotic CMMI stuff pushed by the SEI.
Before you object that there's no math for software engineering, allow me to point out that in fact there is. And it has been used in real world projects. I suggest you look up mathematical approaches such as Z, the B method, VDM, RAISE, or SCR.
With software, for everyone (except Open Source programmers), you are required to use components (OS, compilers, runtime libraries) that are proprietary, can't be inspected, and very often fail to correctly implement what's in the sketchy documentation that's available. You must test everything, so you can discover the underlying failures of the mandated components. If you find that something fails in a critical function, you can beg and plead to have it replaced with something that works, but the vendor can take their good time, or deny your request entirely. Sometimes you can spend extra time rewriting the component, but if it's sufficiently low-level (i.e., inside the OS), this isn't even possible.
So, if you're a programmer, most of your structures are build on unstable, shifting sand. Your tools are inadequate for the job, break at inopportune times. The pieces of your structure fail in unpredictable ways. You are forced to do extensive testing, because engineering calculations just aren't possible when all your materials have unknown defects.
Isn't this really just an argument for greater use of formal methods throughout the software world? The "shifting sand" you mention wouldn't exist if the components you were building on had also been constructed in a mathematically rigorous way.
Sure, engineers test: to validate assumptions about materials, and to check their models. But they still use mathematical models for prediction, because those models allow the verification of a design relative to a much larger set of conditions than could ever be tested for. Software testing for any system of reasonable complexity cannot possibly cover the entire input range or state space. Mathematical modelling of the design has a much better chance of doing so. Will it guarantee that a system will work? No. Will it provide far greater confidence in the design than test alone? Yes. Does it cost any more? No. In fact there's evidence that it is more cost-effective than a test-only strategy.
Spoken like someone who's never worked on a real engineering project outside of the software world. I can't speak to bridge design, but I have designed a few spacecraft in my time (I assume bridges are similar). Spacecraft are very complex. I can assure you that they are very definitely subject to requirements flux. But we spend a lot more time ironing out the requirements in the conceptual design phase. Even then, you can bet that there will be requirements changes further through the design process. It's the use of formal, mathematical models that lets use tame the complexity of the design process, evaluate requirements and designs, and examine the impacts of chnaging requirements.
Are you claiming that the Tacoma Narrows bridge would have worked if they hadn't used formal engineering techniques? I didn't think so. The question isn't whether there are ever failures when using formal, mathematical engineering techniques. The question is: "are there much fewer failures than when not using formal engineering techniques?" The answer, for both bridges and software, is YES.
You are misinterpreting what formal means. It does not mean that you must use a rigid process. It means using math to actually analyze your requiremetns and design. These methods have been used in teh real world to produce radically lower defect rates without incurring significant cost or schedule penalties. Obviously, that's particularly useful for "safety critical" systems, but would presumably be helpful for "normal" software development too.
Formal does not mean "rigid process". It means using mathematical methods to analyze requirements and design. Many "formal design methods" have seen extensive use in the real world: Z, the B method, VDM, CSP, and SCR to name just a few. These are not "ivory tower". They work. They have delivered lower defect rates in the same or less time and cost as informal methods.
Actually there is the issue of availability. Apple has had issues with the supply of PowerPC chips, particularly G5s. On the x86 side of the fence there are no such availability issues as Intel and AMD already have large markets adn produce extremely large volumes.
Given that derivatives of the PowerPC 970 (aka G5) are being used in the X-Box Next and Nintendo's Gamecube follow-on I'm not sure availability will be an issue in the future. Other PowerPC chips are widely used in embedded systems - there's arguably a larger market for the PowerPC architecture (in general) than there is for x86.
Where exactly are the Linux PPC systems?
Well, you could start by looking here.
If they did release for x86 (which would save me $500 asuming it happened now), then they would become in a software company, since their os would have to tackle all the videocards in the market, all the sound cards and so on and so forth.
Apple could decide to use the x86 chips, but keep the system a closed one. Meaning they would still have the tightly integrated hardware/software. But the systems would just use a different chip.
Sure, but then what's the point of moving to x86? The OP, like many others, seems to want OS X on x86 because they somehow think it'll be magically cheaper. It won't unless Apple allowed "beige box" systems. Which they won't. So why keep asking for x86 OS X? There's no advantage to using the x86 architecture aside from a perceived price gain. I'd rather see Windows, Linux, BSD, etc move to the PowerPC architecture.
So in a twisted sense, they are doing the the musicians a favor.
And yet, somehow, the musicians (not just the RIAA) don't seem to see it that way. There are musicians who see free distribution as "a favor". Those are the ones that release their music under licenses that permit re-distribution. The musicians that don't use those kinds of licenses apparently don't think P2P distribution is "a favor". Why don't you let them make their own call on what they consider "a favor"?
Why would they want to release an x86 OS X? The PowerPC is hands-down a better architecture than the x86. And besides, Apple is in the business of selling systems (i.e. an integrated package of hardware and sofwtare), not OS's. I doubt they're about to produce x86-based Macs. And I seriously doubt that they would want to divorce their OS from the integrated system of which it is a part.
I use Gnome and XFCE. But it's not so much the "desktop environment" that provides a superior experience on the Mac, it's the fact that "things just work". I have to exercise far less effort (and Googling) to get something new to work on the Mac than I do under Linux. And that's as much about the underlying OS as it is about the desktop environment.
Which has what to do with military work in space exactly? The original poster was trying to claim that NASA would be getting lots of funding for military work in space. I challenge you to name one NASA space mission (aside from the classified shuttle flights) that was military in nature.
...mess of a system that is still sorely weak in the basics.
Apparently you haven't looked at Mac OS X recently. It has the same "rich base" of command line utils and solid kernel that you claim for Linux. With the additional advantage that "things just work".
I use both Linux and Mac OS X. Right now, I find that, although both have roughly similar capabilites, the Mac gives me a far superior user experience.
Uh, I hate to break it to you, but NASA is a civil agency. They don't do military work, and they don't do "black projects".
NASA does not have a monopoly on government space. The US Air Force does the bulk of the military work in space, along with the National Reconnaissance Office. The Navy also does a little. NASA has nothing to do with military systems such as GPS, DMSP, DSP, Milstar, DCS, TCS, Space Based Laser, SBIRS. They don't even help with the launch: the military has it's own launch facilities at Cape Canaveral and Vandenberg AFB. The only military involvement NASA has ever had is a few classified missions on the shuttle (which were part of the price of getting DoD support for the shuttle program).
I think that the difference lies in the fact that the X-prize was exciting. Most people aren't going to care about "lightweight tethers". Beamed power, maybe. But it doesn't seem like it'd have the same kind of visceral thrill as watching an X-proze competitor launch.
I don't need to. See, there's this thing called "copyright law" that says what you may or may not do with a piece of information that you have acquired. The problem is that so many people ran around breaching the copyright on digital media they had obtained that media companies felt the need to develop a technical solution that enforces copyright law. Does it also trample on "fair use"? Perhaps. The legal definition of "fair use" is a little hazy. If you can suggest a technical solution that permits "fair use", while preventing breach of copyright, I'd love to hear it. As, I'm sure, would many of the media companies. In the mean time, you have the option of purchasing media on the terms that the media companies are willing to supply it under, or not purchasing it at all. Which is precisely the reason that I don't use iTMS.
I don't know about using iTMS (as opposed to the iTunes music player) on Linux, but I suspect it's a no-go at this point (it even took Apple a while to release a Windows version). However, if you do buy tracks from iTMS, you are explicitly allowed to burn them to CD if you want to. Listening to iTMS tracks on an MP3 player isn't directly possible, not because of DRM, but because the tracks are in AAC format, not MP3 (although IIRC the DRM does prevent transcoding). However, if you really want to transcode you can burn your tracks to CD, and then re-rip them to MP3. That is perfectly legit under the iTMS license agreements.
Yes, but that's the point. You aren't buying the music (or other media). You are buying a limited license to use the music (or other media) in some way. If you don't want to buy such a license, don't.
New Zealand: 4 million (Maori also an official language)
Pretty much everyone in New Zealand speaks English. The fact that Maori is an "official language" basically just means that all of the government minitries have Maori names as well as English ones, and Maori shows up in various government-produced documents. Almost no one (if anyone) speaks Maori as a first language, and very few speak it as a second language.
You can read more about the status of English in India here. Sounds like a pretty high percentage of Indians speak English.
You also forgot to include the many other members of the Commonwealth, which, since they are former British colonies, will include a lot of English-speakers. To say nothing of the huge number of Europeans who speak English as a second language. Ditto English-speaking Asians.
I'm not sure I buy Eckel's reasoning on testing vs typing. I dislike the idea of relying on runtime testing to catch errors - the state space is simply too large. IMHO static typing reduces the size of the state space you need to cover in testing, fairly significantly. But he does make some interesting points.
Do these articles (which I frankly don't have the time or energy to look up) actually state that dynamic typing is what provides greater productivity under Python? Or are you just trying to use their general results to back up your specific bias?
Aside: I personally have no stake in this debate either way. I'm just looking for hard information instead of anecdotal opinions.
Slashdot Mirror
Does application of formal methods guarantee zero defects? Of course not. Name any engineering discipline that can guarantee zero defects. There aren't any. As you yourself pointed out, even bridges fall down sometimes. However, I don't think an order of magnitude reduction in defect rates should be ignored. God knows, as a customer, I'd like to see software that doesn't break regulary.
With regard to program scheduling, while I don't think that formal methods are a panacaea, allow me to suggest that if you have no idea what you are doing it is hard to develop a schedule to do it. Doing some mathematical modeling beforehand allows you to gauge the size of the problem. This is how it's done in other engineering disciplines that involve the development of bespoke systems (my own experience in this case is with spacecraft design).
That's not necessarily true:
- I suppose that formal methods are arguably "harder", if by harder you mean "the developer actually has to understand what they are doing". But writing a program is writing a formal specification of what you want the computer to do. The formal methods crowd just advocate writing one or more specifications at a more abstract level as well, preferably in a notation that is amenable either to logical reasoning or mechanical state exploration (or both). The abstract specifications can be considered "prototypes" of the eventual system, that allow one to iron out assumptions and get the overall logic of the software right before you implement all the little details. Which is not to say that you won't revise your abstarct specs later based on things learned during coding - but having multiple layers of abstraction makes it easier to manager the conceptual complexity of the design process. It's really no different than building a bunch of UML models - except that formal models can actually be analyzed, while UML models rely on intuition an visual inspection to verify correctness.
- There's good empirical evidence that formal methods do not actually take any longer than informal methods. Time spent developing formal models is gained back in a shorter test and debug cycle. There are many projects that have used formal methods such as Z or B to produce complex software in the same (or less) time as an equivalent project that does not use formal modeling. Those projects have typically also produced significantly lower defect rates in their delivered software. IBM reported a 9% cost reduction on the CICS project, and a much lower defect rate (although I don't have numbers). Praxis Critical Systems reports reductions in defect rate of up to an order of magnitude (depending on the system) with no increase in cost (see for example the UK CAA's CDIS system, or the Multos Certification Authority).
Are formal methods a silver bullet or panacaea? No.Do formal methods completely eliminate defects? No. But they can reduce their occurrence significantly.
Do formal methods take longer? No.
Do they cost more? No. In fact they can often result in cost savings.
Are formal methods "harder"? Not really.
Why aren't they used more? Because most software "engineers" are scared of learning the (actually relatively straightforward) math involved - it might take the fun out of software development! They'd much rather continue to perpetrate random acts of hackery in the hopes software that passes its unit-tests will continue to function as expected when applied to inputs that fall outside the range of test-cases they have tried.
You're right! Software should be exactly the same!
So why do software "engineers" not use the software analog of the finite element analysis, thermal modeling, combustion analysis, fluid dynamics, and other mathematical modeling that goes into engine design? That's what the grandparent meant by formal methods, not the idiotic CMMI stuff pushed by the SEI.
Before you object that there's no math for software engineering, allow me to point out that in fact there is. And it has been used in real world projects. I suggest you look up mathematical approaches such as Z, the B method, VDM, RAISE, or SCR.
So, if you're a programmer, most of your structures are build on unstable, shifting sand. Your tools are inadequate for the job, break at inopportune times. The pieces of your structure fail in unpredictable ways. You are forced to do extensive testing, because engineering calculations just aren't possible when all your materials have unknown defects.
Isn't this really just an argument for greater use of formal methods throughout the software world? The "shifting sand" you mention wouldn't exist if the components you were building on had also been constructed in a mathematically rigorous way.
Sure, engineers test: to validate assumptions about materials, and to check their models. But they still use mathematical models for prediction, because those models allow the verification of a design relative to a much larger set of conditions than could ever be tested for. Software testing for any system of reasonable complexity cannot possibly cover the entire input range or state space. Mathematical modelling of the design has a much better chance of doing so. Will it guarantee that a system will work? No. Will it provide far greater confidence in the design than test alone? Yes. Does it cost any more? No. In fact there's evidence that it is more cost-effective than a test-only strategy.
Spoken like someone who's never worked on a real engineering project outside of the software world. I can't speak to bridge design, but I have designed a few spacecraft in my time (I assume bridges are similar). Spacecraft are very complex. I can assure you that they are very definitely subject to requirements flux. But we spend a lot more time ironing out the requirements in the conceptual design phase. Even then, you can bet that there will be requirements changes further through the design process. It's the use of formal, mathematical models that lets use tame the complexity of the design process, evaluate requirements and designs, and examine the impacts of chnaging requirements.
Are you claiming that the Tacoma Narrows bridge would have worked if they hadn't used formal engineering techniques? I didn't think so. The question isn't whether there are ever failures when using formal, mathematical engineering techniques. The question is: "are there much fewer failures than when not using formal engineering techniques?" The answer, for both bridges and software, is YES.
You are misinterpreting what formal means. It does not mean that you must use a rigid process. It means using math to actually analyze your requiremetns and design. These methods have been used in teh real world to produce radically lower defect rates without incurring significant cost or schedule penalties. Obviously, that's particularly useful for "safety critical" systems, but would presumably be helpful for "normal" software development too.
Formal does not mean "rigid process". It means using mathematical methods to analyze requirements and design. Many "formal design methods" have seen extensive use in the real world: Z, the B method, VDM, CSP, and SCR to name just a few. These are not "ivory tower". They work. They have delivered lower defect rates in the same or less time and cost as informal methods.
Given that derivatives of the PowerPC 970 (aka G5) are being used in the X-Box Next and Nintendo's Gamecube follow-on I'm not sure availability will be an issue in the future. Other PowerPC chips are widely used in embedded systems - there's arguably a larger market for the PowerPC architecture (in general) than there is for x86.
Where exactly are the Linux PPC systems? Well, you could start by looking here.
Isn't that what I just said?
Sure, but then what's the point of moving to x86? The OP, like many others, seems to want OS X on x86 because they somehow think it'll be magically cheaper. It won't unless Apple allowed "beige box" systems. Which they won't. So why keep asking for x86 OS X? There's no advantage to using the x86 architecture aside from a perceived price gain. I'd rather see Windows, Linux, BSD, etc move to the PowerPC architecture.
And yet, somehow, the musicians (not just the RIAA) don't seem to see it that way. There are musicians who see free distribution as "a favor". Those are the ones that release their music under licenses that permit re-distribution. The musicians that don't use those kinds of licenses apparently don't think P2P distribution is "a favor". Why don't you let them make their own call on what they consider "a favor"?
Why would they want to release an x86 OS X? The PowerPC is hands-down a better architecture than the x86. And besides, Apple is in the business of selling systems (i.e. an integrated package of hardware and sofwtare), not OS's. I doubt they're about to produce x86-based Macs. And I seriously doubt that they would want to divorce their OS from the integrated system of which it is a part.
I use Gnome and XFCE. But it's not so much the "desktop environment" that provides a superior experience on the Mac, it's the fact that "things just work". I have to exercise far less effort (and Googling) to get something new to work on the Mac than I do under Linux. And that's as much about the underlying OS as it is about the desktop environment.
Which has what to do with military work in space exactly? The original poster was trying to claim that NASA would be getting lots of funding for military work in space. I challenge you to name one NASA space mission (aside from the classified shuttle flights) that was military in nature.
Apparently you haven't looked at Mac OS X recently. It has the same "rich base" of command line utils and solid kernel that you claim for Linux. With the additional advantage that "things just work".
I use both Linux and Mac OS X. Right now, I find that, although both have roughly similar capabilites, the Mac gives me a far superior user experience.
NASA does not have a monopoly on government space. The US Air Force does the bulk of the military work in space, along with the National Reconnaissance Office. The Navy also does a little. NASA has nothing to do with military systems such as GPS, DMSP, DSP, Milstar, DCS, TCS, Space Based Laser, SBIRS. They don't even help with the launch: the military has it's own launch facilities at Cape Canaveral and Vandenberg AFB. The only military involvement NASA has ever had is a few classified missions on the shuttle (which were part of the price of getting DoD support for the shuttle program).
I think that the difference lies in the fact that the X-prize was exciting. Most people aren't going to care about "lightweight tethers". Beamed power, maybe. But it doesn't seem like it'd have the same kind of visceral thrill as watching an X-proze competitor launch.
I don't need to. See, there's this thing called "copyright law" that says what you may or may not do with a piece of information that you have acquired. The problem is that so many people ran around breaching the copyright on digital media they had obtained that media companies felt the need to develop a technical solution that enforces copyright law. Does it also trample on "fair use"? Perhaps. The legal definition of "fair use" is a little hazy. If you can suggest a technical solution that permits "fair use", while preventing breach of copyright, I'd love to hear it. As, I'm sure, would many of the media companies. In the mean time, you have the option of purchasing media on the terms that the media companies are willing to supply it under, or not purchasing it at all. Which is precisely the reason that I don't use iTMS.
I don't know about using iTMS (as opposed to the iTunes music player) on Linux, but I suspect it's a no-go at this point (it even took Apple a while to release a Windows version). However, if you do buy tracks from iTMS, you are explicitly allowed to burn them to CD if you want to. Listening to iTMS tracks on an MP3 player isn't directly possible, not because of DRM, but because the tracks are in AAC format, not MP3 (although IIRC the DRM does prevent transcoding). However, if you really want to transcode you can burn your tracks to CD, and then re-rip them to MP3. That is perfectly legit under the iTMS license agreements.
Yes, but that's the point. You aren't buying the music (or other media). You are buying a limited license to use the music (or other media) in some way. If you don't want to buy such a license, don't.
Pretty much everyone in New Zealand speaks English. The fact that Maori is an "official language" basically just means that all of the government minitries have Maori names as well as English ones, and Maori shows up in various government-produced documents. Almost no one (if anyone) speaks Maori as a first language, and very few speak it as a second language.
You can read more about the status of English in India here. Sounds like a pretty high percentage of Indians speak English.
You also forgot to include the many other members of the Commonwealth, which, since they are former British colonies, will include a lot of English-speakers. To say nothing of the huge number of Europeans who speak English as a second language. Ditto English-speaking Asians.
I'm not sure I buy Eckel's reasoning on testing vs typing. I dislike the idea of relying on runtime testing to catch errors - the state space is simply too large. IMHO static typing reduces the size of the state space you need to cover in testing, fairly significantly. But he does make some interesting points.
Aside: I personally have no stake in this debate either way. I'm just looking for hard information instead of anecdotal opinions.