Mailing List Archive Mailing List Archive
Devon, >It's possible to prove formal algorithms but not software. The development > >Trusting algorithms and trusting software are two very different things. > Until recently, you were correct. However, provable specification languages that incorporate all of the tools you mention are in development. The reason that such tools are a little slow in hitting the market, is that the lowest levels must be proven by hand. Then the tool kits are built, up to and including compilers via proven modules. The first commercial product that you will see, in the very near future, will be a CASE type tool that will prove and gurantee function of software to specification. The second level will be proving the hardware. The last will be proving the processors. Expect this cycle to be over within 10 years. The first commercial applications will be out within a year, and provably correct software is currently in development. Probably fodder for other lists, but if you're interested, e-mail me and I'll provide some more details. -- /***************************************************************************/ /* William E. Sadler | email: sadler_b@bs*.bs*.bl*.co* */ /* | batchmo@cr*.co* */ /* Divers Down! [\] | CI$: 71005,1241 */ /* | POTS: (404) 332-2314 */ /***************************************************************************/ /* Keep your Honor, be Bold, and remember: */ /* The only things in the middle of the road are yellow stripes and */ /* squished possums. */ /***************************************************************************/
Navigate by Author:
[Previous]
[Next]
[Author Search Index]
Navigate by Subject:
[Previous]
[Next]
[Subject Search Index]
[Send Reply] [Send Message with New Topic]
[Search Selection] [Mailing List Home] [Home]