Goodbye To Faulty Software?
-
-
http://www.sciencedaily.com/releases/2008/07/080716154355.htm[^] "The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct." Sounds like TDD to me, just with math terms. Write the test then write the code to pass the test.
only two letters away from being an asset
But then some architect would write a framework that removes all types because it is more enterprisey.
Need a C# Consultant? I'm available.
Happiness in intelligent people is the rarest thing I know. -- Ernest Hemingway -
http://www.sciencedaily.com/releases/2008/07/080716154355.htm[^] "The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct." Sounds like TDD to me, just with math terms. Write the test then write the code to pass the test.
only two letters away from being an asset
We know how to write proofs for software. That's not the problem. The problem is that it costs way too much, in both money and time, to do it for any but the most safety-critical software. We also know how to perform enough inspection and testing to catch very large proportions of errors. Again, it's cost-prohibitive. The fact is, our customers don't want to pay for fault-free software. Or, we haven't explained to them just how much it will cost and allowed them to choose the value of this parameter. Proof isn't really compatible with evolutionary development as you really have to have a thorough design to attempt to prove. By the way, your compiler already does some type-theory proving - well, unless you're using a weakly-typed language (like VB with Option Strict off). Most of us don't use a very strong language like Ada because again, defining your own integer types and converting between them as required is time-consuming and hence costly. C++ and C# are strongly-typed for custom types, but there's no concept of different types of integer. I suppose you could design some structures with overloaded operators (e.g. Velocity, Distance, Time: summing any quantity would give the same type, multiplying Velocity and Time gives Distance, etc) but you still have to have access to the raw value to interoperate with any other code. I'd like to see anyone prove a user interface. You're so dependent on your host platform working correctly, which of course you don't have a proof for.
DoEvents: Generating unexpected recursion since 1991
-
-
http://www.sciencedaily.com/releases/2008/07/080716154355.htm[^] "The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct." Sounds like TDD to me, just with math terms. Write the test then write the code to pass the test.
only two letters away from being an asset
Like many of the comments thus far, this is only applicable to safety-critical software that can be formally specified. The problem with 'software' in general is that most of it cannot be formally defined, or, if it were, the errors would still be there -- just abstracted to the formal spec. Also mentioned prevoiously -- try to formally prove a UI design. In my opinion, there is no single software development strategy that applies to all software. For example, the waterfall method requires the specification, design, implementation, all be done completely and correctly (or at least in sequence). This is a greatly inefficient way to develop software that has loosely-stated requirements (and you're never going to get the requirements right anyway)... Agile works only if there is a rapid prototyping framework in place. If you can't quickly build and release components to a target in an embedded environment, this approach becomes ineffective (not to mention the potential CM issues that will arise from any project of more than trivial scope). TDD? Same fate as Agile. So in essence the crux of the problem (i.e. why 'software' hasn't been pinned down like other engineering disciplines) is that the term "software" is all-encompassing and no single method is good for all applications. Don't get me wrong, technologies like Formal Methods has its place, but the idea here is that there is no 'silver bullet' or single process. It comes down to properly scoping a project, selecting the tools and techniques that best suit the project, and establishing adequatre process control such that the effort can be managed -- the continuous balance of cost, schedule, and risk.
~Nitron.
ññòòïðïð**B A
start
** -
http://www.sciencedaily.com/releases/2008/07/080716154355.htm[^] "The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct." Sounds like TDD to me, just with math terms. Write the test then write the code to pass the test.
only two letters away from being an asset
I thought this was going to be about MS dropping support for VB. *sigh*.
-
Like many of the comments thus far, this is only applicable to safety-critical software that can be formally specified. The problem with 'software' in general is that most of it cannot be formally defined, or, if it were, the errors would still be there -- just abstracted to the formal spec. Also mentioned prevoiously -- try to formally prove a UI design. In my opinion, there is no single software development strategy that applies to all software. For example, the waterfall method requires the specification, design, implementation, all be done completely and correctly (or at least in sequence). This is a greatly inefficient way to develop software that has loosely-stated requirements (and you're never going to get the requirements right anyway)... Agile works only if there is a rapid prototyping framework in place. If you can't quickly build and release components to a target in an embedded environment, this approach becomes ineffective (not to mention the potential CM issues that will arise from any project of more than trivial scope). TDD? Same fate as Agile. So in essence the crux of the problem (i.e. why 'software' hasn't been pinned down like other engineering disciplines) is that the term "software" is all-encompassing and no single method is good for all applications. Don't get me wrong, technologies like Formal Methods has its place, but the idea here is that there is no 'silver bullet' or single process. It comes down to properly scoping a project, selecting the tools and techniques that best suit the project, and establishing adequatre process control such that the effort can be managed -- the continuous balance of cost, schedule, and risk.
~Nitron.
ññòòïðïð**B A
start
**Also we overestimate how precise engineering is. I used to work in the oil and gas industry. There are still lots of mistakes but "reliability" is achieved by redundancy.
Kevin
-
http://www.sciencedaily.com/releases/2008/07/080716154355.htm[^] "The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct." Sounds like TDD to me, just with math terms. Write the test then write the code to pass the test.
only two letters away from being an asset
The core part of Scade[^] is written like that - except it uses ML as the implementation language, as it has an almost one-to-one mapping with the specification language. Oh - and don't forget the many, many pages of specification :~. As Mike said we already know how to do this (see CICS[^] - a classic poster boy for formal specification) - it's just that for most systems, the cost completely outweighs the benefit in terms of residual defects. You're probably better off using a language with a higher level of abstraction (Ruby, Python?) so you write less code, on the basis that the less code you write, the less likelihood there is of introducing errors!
-
http://www.sciencedaily.com/releases/2008/07/080716154355.htm[^] "The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct." Sounds like TDD to me, just with math terms. Write the test then write the code to pass the test.
only two letters away from being an asset
This sounds like utter BS to me (it's more likely a way for idiot clever college professors to get grants.)
Anyone who thinks he has a better idea of what's good for people than people do is a swine. - P.J. O'Rourke
-
http://www.sciencedaily.com/releases/2008/07/080716154355.htm[^] "The key lies in an esoteric reformulation of mathematics called ‘type theory’ based on the notion of computation. In this approach, the specification for a computational task is stated as a mathematical theorem. The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct." Sounds like TDD to me, just with math terms. Write the test then write the code to pass the test.
only two letters away from being an asset
:-D
"A Journey of a Thousand Rest Stops Begins with a Single Movement"