One of the things that I got to be quite fond of in Python regexps that I didn't really find a satisfactory replacement for in perl was the ability to create named match groups and then get a group dictionary from the resulting match object. Sure it's just syntactic sugar, but it made pulling out substring matches a lot clearer to read and use by having sensible names for everything.
"And, unlike Perl, it's very easy to do complicated things in simple, legible code."
Perhaps it is time for you to get a perl book or take CS-101 course or something.
It is, I quite agree, entirely possible to write fairly simple clear legible code in perl. It does require a few extra hoops, but in general it isn't that hard, it just requires a fair bit of self-discipline or, if you're working in a team, some very rigid well defined coding standards... that everyone sticks to. From my point of view, if you're at the point of bothering to have and enforce coding standards, why not just enforce them at the language level? The compiler/interpreter can then tell you whether you're meeting appropriate standards, and does a much better job of ensuring everyone actually conforms to a consistent interpretation of the standards. In effect that's what Python does to a certain extent (and you can also find it in other languages like Eiffel and Ada). I perfectly understand that such strict and required enforcement isn't always necessary or desireable - not every software project has maintainability and legibility of code as a primary concern, and if you're just coding by yourself obviously you'll always meet your own standards - but if you are serious about maintainability then, to my mind, language enforced coding standards and a certain amount of "one right way to do it" has real value.
Well I'm not really so sure about your quoted time frames for "re-engineering" Windows - in practice it would porably be easier to start from scratch using best practices from the outset (like, say Singularity). One point does stand out though:
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.
I actually attended a talk by... I think he was Director of Information Assurance... a senior person from the NSA about 5 years on the subject of software assurance. His point was that security, and assurance does matter, and he claimed that, over the next decade, it would become a significant factor in the software industry. It is not working correctly all the time that is important (that would be nice, but isn't sensible or even practical for all software), its having assurance as to what will always work correctly, and/or assurance about the quality of the software suc as you suggest with certification. It's about knowing what it is that you're dealing with. I think the sort of certification you describe, or other guarantees, perhaps with regard to certain critical functions of the software (but not necessarily of the software as a whole), are the way of the future. People who are heading off to college now to learn software engineering really ought to be taking note of the courses on software assurance, formal methods etc. You won't be using it for everything, but I do believe that in the not too distant future you will be expected to know it so you can use it appropriately when required.
I've _never_ met a serious libertarian with those views.
And I freely admit that I've met some particularly whacked out libertarians - the sort that will object to pollution taxes (which are, I agree, a good approach) too. Libertarianism is a pretty diverse political stance, and there are a great many libertarians with whom my views have a lot in common (and where our views differ I respect their point of view). I think, in practice, my views and opinions have been coloured by one too many run ins with the wrong kind, and that's created a natural bias against libertarians in general. I admit that's something I need to work on.
If you want my personal opinion I would tell you that it's an issue with the exceptionally half assed "neither/nor" public/private system that the US uses. Being unwilling to actually commit to either model the system is a patchwork of band-aid fixes that accumulate into a bureaucratic mess that manages to see the worst points of both systems without the benefits of either system.
Considering that insurance is heavily abused by millions, I think they should investigate claims. In the past, insurance was something one used for emergencies.
And why is insurance abused by millions? Why do they not reserve insurance claims for emergencies? I don't think that's the governments doing, I think that's simply the state of the culture - a different value system than yours that clearly doesn't feel that waiting for emergencies is the right approach, and that it's worth at least trying to scam the system. Now I understand you are clearly not going to try and force everyone else to take up your value system, so you are going to have people doing their best to scam the system, and that is going to force up administrative costs for private insurance companies who have to try and weed out the freeloaders. Moving from public to private does not remove the freeloaders from the system. Eliminating the public system will simply drive the freeloaders into the private system. Your only benefit there is that you are imposing a minimum threshold before people can even join that system - presumably all the others can try and find some other way to scam the system, robbery perhaps.
You'd hope so, but they're bascially cowboy anarchists. The minimal role that they do see for government is arguably inconsistent with their "fend for yourself" vision of freedom. Why, for instance, should the state protect me from the use of force by others but not from pollution of the air by others?
Many libertarians would claim they do provide protection, it's just that the protection is retributive rather than preventive. By the sort of legal system I've heard proposed by some libetertarians it would be quite legal for me to empty a clip from a machine gun into a busy kindergarten playground. Now I might get into trouble if by some accident I actually happened to hit a child, but there's absolutely nothing stopping me from trying, and if I do miss then I have done nothing wrong. The same applies to pollution - if I don't happen to actually do any harm that anyone actaully notices then it simply doesn't matter. The fact that the harm may be irreversible by the time someone does notice doesn't enter into it. The belief, as far as I can tell, is that the threat of retribution is enough to stop people from trying. Of course that tends to presume rational judgment on the part of the individual considering the action and, I would guess, people inclined to spray gunfire at a kindergarten are not especially rational.
In essence: Yes the government has a monopoly on force. That's actually preferable to a free market for force, which is what you'll get unless you can somehow convince absolutely everyone to forgo the use of force (which you won't).
I would hope that even libertarians recognise that there is a distinct place for government. Once we've gotten past that, we can get down to the more debatable, and variable, question of exactly how much government control is valuable.
Sidebar: "Papers must be formatted using the provided LaTeX template" This seems a bit old skool to me. I've been out of the academic loop for a few years now, but is this standard now? Even for a Linux Love Fest this seems like a bit of a constraint...
Obviously you're not in mathematics. I can't speak for other disciplines but it is quite common for math conferences to have have formatting templates... and no serious mathematics paper is going to be formatted in something other than a TeX based system, so LaTeX is pretty standard.
My money is on the Apple Tablet being unveiled.... but maybe that's just wishful thinking.
What I would like to see is something like a G5 iMac with wireless keyboard and mouse and a touch screen (and, I guess, some sort of handwriting recognition) as the "Apple Tablet". Most of the time it can sit on it's stand charging and being an ordinary desktop machine, but you can pick it up and carry it to the couch to read, watch a movie or do other less keyboard intensive tasks (anything that requires only occasional notes/typing, like annotating/editing a document instead of writing it). In that sense you're not buying a "tablet", you're just buying an ordinary iMac... it just happens to have the benefits of a tablet when you want it.
I think, to be honest, that all that was really shown is that popular modern Linux desktop distributions are targetted at modern hardware, and as a result don't run as well on older hardware. They ran Red Hat and Mandrake and Novell etc. 'out of the box' with no customisation to make it fit with the hardware - unsurprisingly the default install of such distros a targetted at modern systems and have hefty system requirements.
Pick up a distribution that actually claims to target older hardware, or just generally fit in smaller places, like say Damn Small Linux, Feather Linux or Zenwalk and I suspect you'll find much better performance and much lower system requirements all 'out of the box'. The counter-claim seems to be that Windows CE, with the right customisations, will run on older hardware too. Does anyone know if their is a release of CE set up for desktop use on older hardwre?
It really depends on what you are writing. If you're implementing a security protocol, or a network service, then taking the extra time to spell things out and be able to prove there aren't any buffer overflows is probably entirely worth your time.
For projects that aren't as critical you can still get significant benefits from a slightly scaled back approach - things like Design by Contract help developers to spell out their intentions more clearly and can go a long way toward catching and isolating bugs earlier. If you're using the right tools (like, say JML combined with ESC/Java2) you can even do extended static checking and catch a lot of other bugs, where what you've coded doesn't match your stated intentions (usually in the form of annotations) much, much earlier.
No, there's no silver bullet. That doesn't mean, however, that there aren't things that can be done that make things better than they are now.
That sounds great and all, but do you have any idea of the complexity, and therefore cost involved? Ever tried to debug something consisting of 10000 lines, let alone something the size of an OS?
Interestingly there was just an article about exceptionally low defect rates for software, with cases running from a mere 10,000 up to almost 200,000 SLOC, all done for very reasonable time frames and costs. That, of course, is still signficantly less than the complexity of, say, the entire Linux kernel - but then no one said the whole thing had to be perfect, why not just start with the critical parts? Does it matter if every single obscure device driver is perfect? Under the circumstances that's forgivable, and porbably isn't so important. Making sure the core parts are exploit free using solid techniques does make some sense though. There are such projects underway - see Coyotos and Singularity.
a better goal is to ensure that when bugs are found they have minimal impact (like ensure users aren't running as root)
Indeed, but we can do better than this - there are more modern architectures for isolating problems, and they are available right now in Linux, SELinux being the most visible example. The problem is that right now applications often aren't written to respect, or take advantage of the benefits SELinux offers, so the improvement just isn't that great (a very loose policy is required). That is to say Linux is in a state with SELinux similar to where Windows is with Administrator accounts: the technology is there, and if used would represent a huge step in improving security, but because of lagging applications and users it's failing to take the required steps to e more secure.
Then their ability to produce bug-free code depends, as usual, on control factors, not on real-world engineering.
In as much as a civil engineer depends on control factors via refusing customers who demand that the building have 6 stories not 4 just one month before construction is due to finish, yes. Real world engineering makes certain demands of the client. Someone who wants to build a treehouse for their kids doesn't consult an architect and a civil engineer, and civil engineers don't take contracts from people who refuse to set out some limits on what they want built, and what they expect of it.
Praxis uses solid engineering. Their "Correct by Construction" approach is solidly grounded in axiomatic mathematics and uses similar sorts of formal calculations and logical and mathematical proofs as you might expect to see from civil, electrical, aerospace, or ny other kind of engineers. Take the time to read sample chapters from the SPARK book to get an idea of exactly what they are doing. There is very definitely quite solid engineering going on.
I RTFA to the point where they started putting restrictions on languages of choice and then I stopped. I don't disagree. I just realize the article applies less to my work than I thought.
Well there are options you can take that aren't the whole hog of SPARK Ada with it's restrictions and formality. If you just want to make things clearer and get some of the benefits then for Java there's JML which provides similar annotation syntax to SPARK and comes with some freely available tools to convert annotations into JUnit tests, runtime assertions, and include them in JavaDoc documentation. There's also ESC/Java2 which provides extended static checking based on JML annotations.
If you are using C# then there's Spec# which, again, provides similar annotation and basic tool support to C#, kindly provided by Microsoft. If you're using C++ mostly there's C2, or if you don't want payware then you could look into D which provides Design by Contract - it is a language shift, but not too huge a one. Then there's always Eiffel.
If you are more of functional programmer then there's Extended ML or HasCASL which both seek to being some of the benefits of algebraic specification to functional languages (in this case Standard ML and Haskell).
So all up you aren't as pinned to a language as it might first appear - depending on how important correctness is there are a variety of options in a wide variety of languages.
And why are softwares so buggy and have such a lousy reputation anyway? Not to start a flamewar, but let's just list a few possible "reaons" here:
I think, to be honest, that it is a combination of a number of the factors you mention.
Why aren't schools teaching this methodoly thoroughly? Why aren't this toolset and programming language taught in school by default?
To do proper formal specification, one of the key parts of Praxis' Correct by Construction approach, does require a decent solid mathematical background. I think a lot of CS departments, facing students who want vocational training, struggle to demand the sort of mathematical requirements that are needed. As to SPARK - it is something that Praxis developed themselves, and it is proprietary (the toolset at least, the annotation language is well documented). You can pick up a book and learn the language, but the tools cost money if you want to use them commercially. On the other hand, the base specification language Praxis uses, Z, is entirely open, and there are a variety of freely available tools for it. There are also other specification langauges (I quite like CASL which has a number of useful extensions) that have freely available tools associated with them. There's also JML and ESC/Java2 which are freely available and seek to provide the same sort of functionality or Java that SPARK adds to Ada. There are places that teach JML, but they are still few and far between.
Programmers are asked to do the impossible.
I think this is a big part of it in some ways. Partly this is because, for a large number of software projects, the degree of exactness and quality just isn't required. I don't need a professional architect to help me build a doghouse in my backyard (though I'd certainly want one if I was building a skyscraper), and I don't need assurances of bug free software for a simple web front-end to a database. At the same time programmers are often unwilling to let customers know exactly what the limits are when developing software. To quote you: "If a customer dares to ask a civil engineer to add 2 more stories between the 3rd and 4th floor after the custom-built building is finished, guess what would the civil engineer say?"; if software engineers aren't prepared to stand up for quality and tell customers that somethings can't be done without sacrificing the quality of the product the problem will remain. In part I think this is due to the fact that software development is a young industry, and programmers are still of the mentality that they need to do everything they possibly can to please a customer. Partly it's because software projects are diverse (as are building projects!) and sometimes it's okay to make late changes; sometimes it's how things ought to be done - the key is to identify exactly what sort of project it is as early as you can. Are you building a treehouse for your kids, which doesn't require exactness and benefits from incremental design and feedback, or are you building a 4 story building where quality is important, and late changes will jepordise that?
Programmers are a bunch of bozos who know shit about proper engineering.
Sadly this is partly the case. There are an awful lot of cowboys out there when it comes to software engineering. There are, of course, a lot of fantastic programmers as well who are otherwise beset by some of the other points mentioned. There is, however, a remarkable degree of tolerance for cowboys, sloppiness and lack of quality in software engineering that you don't see in other engineering disciplines. Partly I thin
While that's a good an interesting article, I would like to point out that what these articles about Praxis and their methodology are talking about is slightly different. Praxis doesn't have the same rigid process and "big design up front" approach of the shuttle team, nor do they require the sort of expense mentioned. They do, however, have the same professionalism and mathematical rigor in developing their code.
It's very true that developing quality code is something that requires both parties commitment. If someone is unwilling to work with the developers to help them clearly define the requirements then yes, quality code is going to be all but impossible, and in that case it isn't the developer's fault. As others have pointed out, a large part of the reason so much code is so bad is simply because the clients fail to demand a higher standard. As long as customer expectations are low, or they are unwilling to actually commit to getting good results, there will remain issues.
Wouldn't UML help with engineering? It's designed of this purpose. You can UML anything, and reports have it that UML makes it easier to find bugs, and make deadlines.
Praxis tends to use a more rigorous and exacting modelling/specification language called Z. It's a formalised mathematical specification language that allows for exceptionally precise documentation of formal requirements. When translating the specification into code Praxis uses SPARK a programming language specifically designed to allow the incorporation of formal specification into the code, and with a very powerful set of tools for static analysis of the code and specification.
I have noticed that nobody really asked. What type of application are they writing?
As stated in the article, they are develping things like air traffic control systems, authentication systems to run on smart cards for international credit card companies etc. Their projects run into the hundreds of thousands of lines of code. These are not simple or trivial applications.
It is much easier to write bug free code if the problems you solve have limited scope. The usual problem with solutions of this type is that they solve the problem the user described and not the actually much more complex the problem the user actually needs solved. For example, a user could say I need a way to view marked up text and graphics in a windows application. What he does not know is that he really needs a complex solution like Firefox which supports CSS, javascript, AJAX, plugin architectures and so on.
Again, the article does discuss this to some extent, but a major part of their development process is working closely with the customer to manage to develop a clear set of requirements. This can, of course, be a time consuming process, and is naturally going to be ongoing to some extent through the project. The key is to try and get much of it done as early as possible. That involves sitting down with the customer and working out what it actually is they require. So when the user says they "need a way to view marked up text and graphics in a windows application" it behoves the person developing the requirements to ask questions like "Do you need to be able to have interactive views?", "What sorts of interaction do you need, and does it need to conform to a standard? If so, which one?", "Is it acceptable if this aspect of Javascript isn't implemented - that would mean that things like X would be impossible?" and so on. The aim is to build up a set of unambiguous formal requirements. Skipping the phase where you try and work ith the customer to understand in detail what they actually want - well that's always a recipe for disaster. In many ways that's what things like Agile Development are all about. This is similar, but tries to develop a formal specification rather than an incremental prototype.
Yes, small teams help, but I think it really is worth taking a look at the tools and methods that Praxis uses because there are some remarkably good ideas in there. Take a look at SPARK Ada - the Wikipedia article has some basic examples, and Praxis provides sample chapters of a book on SPARK for download. Seriously, take a little time out of your day, sit down, and read a little about how they do what they do. There really are good ideas that go well beyond just "small teams" if you want to deliver correctly functioning code.
Also, how many of you have ever had a customer who could state their requirements clearly enough to offer that kind of warranty?
Clearly the sort of assurances that Praxis provides aren't reasonable for every project, but then again not every project really requires that degree of assurance. There are, however, a great many software projects, particularly security or network related ones, that could almost definitely benefit from the sort of approach Praxis takes. Those projects are also, usually, entirely capable of working with the client to develop a clear an unambiguous set of requirements.
But what very many bugs boil down to, when not typos (which is surprisingly common) is: "Hey, I didn't think about that ever happening, and that it would have those consequences.".
This is why Praxis uses formal specification, which is a method for formally writing down your requirements in a way that tends to make the things you didn't otherwise think about clear. You can find some of my thoughts of formal specification here. Just using something as simple as preconditions and postconditions can help alleviate much of the problem by simply making quite explicit exactly what it is you are expecting, and giving anyone who calls the function a clear indication of exactly what they can safely assume your function will return. It's precisely these sorts of techniques - simple but effective - that can help reduce errors. Take a look at projects developed in Eiffel which has strong Design by Contract syntax providing pre and postconditions and you'll already see a reduction in the rate of bugs. Take the formalism further, as Praxis does using SPARK, and you'll see stunning results.
Jedidiah.
Re:The right programming language helps hugely
on
When Bugs Aren't Allowed
·
· Score: 4, Informative
Praxis uses SPARK Ada, which is a subset of the Ada programming language and annotations that provide for extended static checking, and theorem proving. You can find more about SPARK at the Praxis website, or the Wikipedia article isn't too bad. It's a very nice language, and has fantastic tool support.
If you find that interesting, but Ada isn't to your taste, you can try JML for Java which provides similar (but lacking quite the same robustness and tool support) annotations. JML lets you automatically generate JUnit tests based on your annotations, and with ESC/Java2 allows for extended static checking.
If, as you appear, you are more of a fan of functional languages then I'd suggest you check out Extended ML and HasCASL which provide similar sorts of formal specification capabilities for ML and Haskell. Tool support for these is still a little limited, but they are both quite powerful and provide very expressive specification syntax.
Slashdot Mirror
One of the things that I got to be quite fond of in Python regexps that I didn't really find a satisfactory replacement for in perl was the ability to create named match groups and then get a group dictionary from the resulting match object. Sure it's just syntactic sugar, but it made pulling out substring matches a lot clearer to read and use by having sensible names for everything.
Jedidiah.
"And, unlike Perl, it's very easy to do complicated things in simple, legible code."
... that everyone sticks to. From my point of view, if you're at the point of bothering to have and enforce coding standards, why not just enforce them at the language level? The compiler/interpreter can then tell you whether you're meeting appropriate standards, and does a much better job of ensuring everyone actually conforms to a consistent interpretation of the standards. In effect that's what Python does to a certain extent (and you can also find it in other languages like Eiffel and Ada). I perfectly understand that such strict and required enforcement isn't always necessary or desireable - not every software project has maintainability and legibility of code as a primary concern, and if you're just coding by yourself obviously you'll always meet your own standards - but if you are serious about maintainability then, to my mind, language enforced coding standards and a certain amount of "one right way to do it" has real value.
Perhaps it is time for you to get a perl book or take CS-101 course or something.
It is, I quite agree, entirely possible to write fairly simple clear legible code in perl. It does require a few extra hoops, but in general it isn't that hard, it just requires a fair bit of self-discipline or, if you're working in a team, some very rigid well defined coding standards
Jedidiah.
Either that, or there's some bizarre plot against Finland afoot...
Hmm, I think i'll go with your explanation.
Jedidiah.
Thoughts?
Well I'm not really so sure about your quoted time frames for "re-engineering" Windows - in practice it would porably be easier to start from scratch using best practices from the outset (like, say Singularity). One point does stand out though:
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.
I actually attended a talk by... I think he was Director of Information Assurance... a senior person from the NSA about 5 years on the subject of software assurance. His point was that security, and assurance does matter, and he claimed that, over the next decade, it would become a significant factor in the software industry. It is not working correctly all the time that is important (that would be nice, but isn't sensible or even practical for all software), its having assurance as to what will always work correctly, and/or assurance about the quality of the software suc as you suggest with certification. It's about knowing what it is that you're dealing with. I think the sort of certification you describe, or other guarantees, perhaps with regard to certain critical functions of the software (but not necessarily of the software as a whole), are the way of the future. People who are heading off to college now to learn software engineering really ought to be taking note of the courses on software assurance, formal methods etc. You won't be using it for everything, but I do believe that in the not too distant future you will be expected to know it so you can use it appropriately when required.
Jedidiah.
I've _never_ met a serious libertarian with those views.
And I freely admit that I've met some particularly whacked out libertarians - the sort that will object to pollution taxes (which are, I agree, a good approach) too. Libertarianism is a pretty diverse political stance, and there are a great many libertarians with whom my views have a lot in common (and where our views differ I respect their point of view). I think, in practice, my views and opinions have been coloured by one too many run ins with the wrong kind, and that's created a natural bias against libertarians in general. I admit that's something I need to work on.
Jedidiah.
If you want my personal opinion I would tell you that it's an issue with the exceptionally half assed "neither/nor" public/private system that the US uses. Being unwilling to actually commit to either model the system is a patchwork of band-aid fixes that accumulate into a bureaucratic mess that manages to see the worst points of both systems without the benefits of either system.
Jedidiah.
Considering that insurance is heavily abused by millions, I think they should investigate claims. In the past, insurance was something one used for emergencies.
And why is insurance abused by millions? Why do they not reserve insurance claims for emergencies? I don't think that's the governments doing, I think that's simply the state of the culture - a different value system than yours that clearly doesn't feel that waiting for emergencies is the right approach, and that it's worth at least trying to scam the system. Now I understand you are clearly not going to try and force everyone else to take up your value system, so you are going to have people doing their best to scam the system, and that is going to force up administrative costs for private insurance companies who have to try and weed out the freeloaders. Moving from public to private does not remove the freeloaders from the system. Eliminating the public system will simply drive the freeloaders into the private system. Your only benefit there is that you are imposing a minimum threshold before people can even join that system - presumably all the others can try and find some other way to scam the system, robbery perhaps.
Jedidiah.
You'd hope so, but they're bascially cowboy anarchists. The minimal role that they do see for government is arguably inconsistent with their "fend for yourself" vision of freedom. Why, for instance, should the state protect me from the use of force by others but not from pollution of the air by others?
Many libertarians would claim they do provide protection, it's just that the protection is retributive rather than preventive. By the sort of legal system I've heard proposed by some libetertarians it would be quite legal for me to empty a clip from a machine gun into a busy kindergarten playground. Now I might get into trouble if by some accident I actually happened to hit a child, but there's absolutely nothing stopping me from trying, and if I do miss then I have done nothing wrong. The same applies to pollution - if I don't happen to actually do any harm that anyone actaully notices then it simply doesn't matter. The fact that the harm may be irreversible by the time someone does notice doesn't enter into it. The belief, as far as I can tell, is that the threat of retribution is enough to stop people from trying. Of course that tends to presume rational judgment on the part of the individual considering the action and, I would guess, people inclined to spray gunfire at a kindergarten are not especially rational.
Jedidiah.
In essence: Yes the government has a monopoly on force. That's actually preferable to a free market for force, which is what you'll get unless you can somehow convince absolutely everyone to forgo the use of force (which you won't).
I would hope that even libertarians recognise that there is a distinct place for government. Once we've gotten past that, we can get down to the more debatable, and variable, question of exactly how much government control is valuable.
Jedidiah.
Sidebar: "Papers must be formatted using the provided LaTeX template" This seems a bit old skool to me. I've been out of the academic loop for a few years now, but is this standard now? Even for a Linux Love Fest this seems like a bit of a constraint...
Obviously you're not in mathematics. I can't speak for other disciplines but it is quite common for math conferences to have have formatting templates... and no serious mathematics paper is going to be formatted in something other than a TeX based system, so LaTeX is pretty standard.
Jedidiah.
My money is on the Apple Tablet being unveiled. ... but maybe that's just wishful thinking.
What I would like to see is something like a G5 iMac with wireless keyboard and mouse and a touch screen (and, I guess, some sort of handwriting recognition) as the "Apple Tablet". Most of the time it can sit on it's stand charging and being an ordinary desktop machine, but you can pick it up and carry it to the couch to read, watch a movie or do other less keyboard intensive tasks (anything that requires only occasional notes/typing, like annotating/editing a document instead of writing it). In that sense you're not buying a "tablet", you're just buying an ordinary iMac... it just happens to have the benefits of a tablet when you want it.
Jedidiah.
I think, to be honest, that all that was really shown is that popular modern Linux desktop distributions are targetted at modern hardware, and as a result don't run as well on older hardware. They ran Red Hat and Mandrake and Novell etc. 'out of the box' with no customisation to make it fit with the hardware - unsurprisingly the default install of such distros a targetted at modern systems and have hefty system requirements.
Pick up a distribution that actually claims to target older hardware, or just generally fit in smaller places, like say Damn Small Linux, Feather Linux or Zenwalk and I suspect you'll find much better performance and much lower system requirements all 'out of the box'. The counter-claim seems to be that Windows CE, with the right customisations, will run on older hardware too. Does anyone know if their is a release of CE set up for desktop use on older hardwre?
Jedidiah.
It really depends on what you are writing. If you're implementing a security protocol, or a network service, then taking the extra time to spell things out and be able to prove there aren't any buffer overflows is probably entirely worth your time.
For projects that aren't as critical you can still get significant benefits from a slightly scaled back approach - things like Design by Contract help developers to spell out their intentions more clearly and can go a long way toward catching and isolating bugs earlier. If you're using the right tools (like, say JML combined with ESC/Java2) you can even do extended static checking and catch a lot of other bugs, where what you've coded doesn't match your stated intentions (usually in the form of annotations) much, much earlier.
No, there's no silver bullet. That doesn't mean, however, that there aren't things that can be done that make things better than they are now.
Jedidiah.
That sounds great and all, but do you have any idea of the complexity, and therefore cost involved? Ever tried to debug something consisting of 10000 lines, let alone something the size of an OS?
Interestingly there was just an article about exceptionally low defect rates for software, with cases running from a mere 10,000 up to almost 200,000 SLOC, all done for very reasonable time frames and costs. That, of course, is still signficantly less than the complexity of, say, the entire Linux kernel - but then no one said the whole thing had to be perfect, why not just start with the critical parts? Does it matter if every single obscure device driver is perfect? Under the circumstances that's forgivable, and porbably isn't so important. Making sure the core parts are exploit free using solid techniques does make some sense though. There are such projects underway - see Coyotos and Singularity.
a better goal is to ensure that when bugs are found they have minimal impact (like ensure users aren't running as root)
Indeed, but we can do better than this - there are more modern architectures for isolating problems, and they are available right now in Linux, SELinux being the most visible example. The problem is that right now applications often aren't written to respect, or take advantage of the benefits SELinux offers, so the improvement just isn't that great (a very loose policy is required). That is to say Linux is in a state with SELinux similar to where Windows is with Administrator accounts: the technology is there, and if used would represent a huge step in improving security, but because of lagging applications and users it's failing to take the required steps to e more secure.
Jedidiah.
Then their ability to produce bug-free code depends, as usual, on control factors, not on real-world engineering.
In as much as a civil engineer depends on control factors via refusing customers who demand that the building have 6 stories not 4 just one month before construction is due to finish, yes. Real world engineering makes certain demands of the client. Someone who wants to build a treehouse for their kids doesn't consult an architect and a civil engineer, and civil engineers don't take contracts from people who refuse to set out some limits on what they want built, and what they expect of it.
Praxis uses solid engineering. Their "Correct by Construction" approach is solidly grounded in axiomatic mathematics and uses similar sorts of formal calculations and logical and mathematical proofs as you might expect to see from civil, electrical, aerospace, or ny other kind of engineers. Take the time to read sample chapters from the SPARK book to get an idea of exactly what they are doing. There is very definitely quite solid engineering going on.
I RTFA to the point where they started putting restrictions on languages of choice and then I stopped. I don't disagree. I just realize the article applies less to my work than I thought.
Well there are options you can take that aren't the whole hog of SPARK Ada with it's restrictions and formality. If you just want to make things clearer and get some of the benefits then for Java there's JML which provides similar annotation syntax to SPARK and comes with some freely available tools to convert annotations into JUnit tests, runtime assertions, and include them in JavaDoc documentation. There's also ESC/Java2 which provides extended static checking based on JML annotations.
If you are using C# then there's Spec# which, again, provides similar annotation and basic tool support to C#, kindly provided by Microsoft. If you're using C++ mostly there's C2, or if you don't want payware then you could look into D which provides Design by Contract - it is a language shift, but not too huge a one. Then there's always Eiffel.
If you are more of functional programmer then there's Extended ML or HasCASL which both seek to being some of the benefits of algebraic specification to functional languages (in this case Standard ML and Haskell).
So all up you aren't as pinned to a language as it might first appear - depending on how important correctness is there are a variety of options in a wide variety of languages.
Jedidiah.
Thanks for a thoughtful post.
And why are softwares so buggy and have such a lousy reputation anyway? Not to start a flamewar, but let's just list a few possible "reaons" here:
I think, to be honest, that it is a combination of a number of the factors you mention.
Why aren't schools teaching this methodoly thoroughly? Why aren't this toolset and programming language taught in school by default?
To do proper formal specification, one of the key parts of Praxis' Correct by Construction approach, does require a decent solid mathematical background. I think a lot of CS departments, facing students who want vocational training, struggle to demand the sort of mathematical requirements that are needed. As to SPARK - it is something that Praxis developed themselves, and it is proprietary (the toolset at least, the annotation language is well documented). You can pick up a book and learn the language, but the tools cost money if you want to use them commercially. On the other hand, the base specification language Praxis uses, Z, is entirely open, and there are a variety of freely available tools for it. There are also other specification langauges (I quite like CASL which has a number of useful extensions) that have freely available tools associated with them. There's also JML and ESC/Java2 which are freely available and seek to provide the same sort of functionality or Java that SPARK adds to Ada. There are places that teach JML, but they are still few and far between.
Programmers are asked to do the impossible.
I think this is a big part of it in some ways. Partly this is because, for a large number of software projects, the degree of exactness and quality just isn't required. I don't need a professional architect to help me build a doghouse in my backyard (though I'd certainly want one if I was building a skyscraper), and I don't need assurances of bug free software for a simple web front-end to a database. At the same time programmers are often unwilling to let customers know exactly what the limits are when developing software. To quote you: "If a customer dares to ask a civil engineer to add 2 more stories between the 3rd and 4th floor after the custom-built building is finished, guess what would the civil engineer say?"; if software engineers aren't prepared to stand up for quality and tell customers that somethings can't be done without sacrificing the quality of the product the problem will remain. In part I think this is due to the fact that software development is a young industry, and programmers are still of the mentality that they need to do everything they possibly can to please a customer. Partly it's because software projects are diverse (as are building projects!) and sometimes it's okay to make late changes; sometimes it's how things ought to be done - the key is to identify exactly what sort of project it is as early as you can. Are you building a treehouse for your kids, which doesn't require exactness and benefits from incremental design and feedback, or are you building a 4 story building where quality is important, and late changes will jepordise that?
Programmers are a bunch of bozos who know shit about proper engineering.
Sadly this is partly the case. There are an awful lot of cowboys out there when it comes to software engineering. There are, of course, a lot of fantastic programmers as well who are otherwise beset by some of the other points mentioned. There is, however, a remarkable degree of tolerance for cowboys, sloppiness and lack of quality in software engineering that you don't see in other engineering disciplines. Partly I thin
While that's a good an interesting article, I would like to point out that what these articles about Praxis and their methodology are talking about is slightly different. Praxis doesn't have the same rigid process and "big design up front" approach of the shuttle team, nor do they require the sort of expense mentioned. They do, however, have the same professionalism and mathematical rigor in developing their code.
Jedidiah.
It's very true that developing quality code is something that requires both parties commitment. If someone is unwilling to work with the developers to help them clearly define the requirements then yes, quality code is going to be all but impossible, and in that case it isn't the developer's fault. As others have pointed out, a large part of the reason so much code is so bad is simply because the clients fail to demand a higher standard. As long as customer expectations are low, or they are unwilling to actually commit to getting good results, there will remain issues.
Jedidiah.
Wouldn't UML help with engineering? It's designed of this purpose. You can UML anything, and reports have it that UML makes it easier to find bugs, and make deadlines.
Praxis tends to use a more rigorous and exacting modelling/specification language called Z. It's a formalised mathematical specification language that allows for exceptionally precise documentation of formal requirements. When translating the specification into code Praxis uses SPARK a programming language specifically designed to allow the incorporation of formal specification into the code, and with a very powerful set of tools for static analysis of the code and specification.
Jedidiah.
I have noticed that nobody really asked. What type of application are they writing?
As stated in the article, they are develping things like air traffic control systems, authentication systems to run on smart cards for international credit card companies etc. Their projects run into the hundreds of thousands of lines of code. These are not simple or trivial applications.
It is much easier to write bug free code if the problems you solve have limited scope. The usual problem with solutions of this type is that they solve the problem the user described and not the actually much more complex the problem the user actually needs solved. For example, a user could say I need a way to view marked up text and graphics in a windows application. What he does not know is that he really needs a complex solution like Firefox which supports CSS, javascript, AJAX, plugin architectures and so on.
Again, the article does discuss this to some extent, but a major part of their development process is working closely with the customer to manage to develop a clear set of requirements. This can, of course, be a time consuming process, and is naturally going to be ongoing to some extent through the project. The key is to try and get much of it done as early as possible. That involves sitting down with the customer and working out what it actually is they require. So when the user says they "need a way to view marked up text and graphics in a windows application" it behoves the person developing the requirements to ask questions like "Do you need to be able to have interactive views?", "What sorts of interaction do you need, and does it need to conform to a standard? If so, which one?", "Is it acceptable if this aspect of Javascript isn't implemented - that would mean that things like X would be impossible?" and so on. The aim is to build up a set of unambiguous formal requirements. Skipping the phase where you try and work ith the customer to understand in detail what they actually want - well that's always a recipe for disaster. In many ways that's what things like Agile Development are all about. This is similar, but tries to develop a formal specification rather than an incremental prototype.
Jedidiah.
Yes, small teams help, but I think it really is worth taking a look at the tools and methods that Praxis uses because there are some remarkably good ideas in there. Take a look at SPARK Ada - the Wikipedia article has some basic examples, and Praxis provides sample chapters of a book on SPARK for download. Seriously, take a little time out of your day, sit down, and read a little about how they do what they do. There really are good ideas that go well beyond just "small teams" if you want to deliver correctly functioning code.
Jedidiah.
Also, how many of you have ever had a customer who could state their requirements clearly enough to offer that kind of warranty?
Clearly the sort of assurances that Praxis provides aren't reasonable for every project, but then again not every project really requires that degree of assurance. There are, however, a great many software projects, particularly security or network related ones, that could almost definitely benefit from the sort of approach Praxis takes. Those projects are also, usually, entirely capable of working with the client to develop a clear an unambiguous set of requirements.
Jedidiah.
But what very many bugs boil down to, when not typos (which is surprisingly common) is: "Hey, I didn't think about that ever happening, and that it would have those consequences.".
This is why Praxis uses formal specification, which is a method for formally writing down your requirements in a way that tends to make the things you didn't otherwise think about clear. You can find some of my thoughts of formal specification here. Just using something as simple as preconditions and postconditions can help alleviate much of the problem by simply making quite explicit exactly what it is you are expecting, and giving anyone who calls the function a clear indication of exactly what they can safely assume your function will return. It's precisely these sorts of techniques - simple but effective - that can help reduce errors. Take a look at projects developed in Eiffel which has strong Design by Contract syntax providing pre and postconditions and you'll already see a reduction in the rate of bugs. Take the formalism further, as Praxis does using SPARK, and you'll see stunning results.
Jedidiah.
Praxis uses SPARK Ada, which is a subset of the Ada programming language and annotations that provide for extended static checking, and theorem proving. You can find more about SPARK at the Praxis website, or the Wikipedia article isn't too bad. It's a very nice language, and has fantastic tool support.
If you find that interesting, but Ada isn't to your taste, you can try JML for Java which provides similar (but lacking quite the same robustness and tool support) annotations. JML lets you automatically generate JUnit tests based on your annotations, and with ESC/Java2 allows for extended static checking.
If, as you appear, you are more of a fan of functional languages then I'd suggest you check out Extended ML and HasCASL which provide similar sorts of formal specification capabilities for ML and Haskell. Tool support for these is still a little limited, but they are both quite powerful and provide very expressive specification syntax.
Jedidiah.