[
Lists Home |
Date Index |
Thread Index
]
While this thread seems to be devolving into talk about degrees and
"principles of software engineering" :) I think there is one important
facet of "safe" software that is being left out - that there is already
a well developed software and research community about safe software.
Dangerous software errors can happen - and these can be especially
dangerous in military systems, for example Missle Defense programs
(see Brian Cantwell Smith, a founder of Computer Professionals for Social
Responsibility, essay on the subject "Limits of Correctness,
http://portal.acm.org/citation.cfm?id=379512).
However, using methods from formal proof proving systems to
verify the output of your program is useful, and there is little of this
done in the XML community. In a simple example just think of the bugs
caught by type checking in your average C compiler. Thus, the move in
languages like XQuery to a formal semantics may seem somewhat obscure to
anyone but compiler developers and standard tweakers, but having a
programming language with a solid formal foundation allows proofs to be
made about the correctness of programs, which can in turn prevent errors.
I suggest reading George Porter's essay for a gentle qualitative
introduction:
http://www.cs.berkeley.edu/~gporter/pubs/roleofproof.html
And I suggest taking a look at not only XQuery but the mature research
community around Standard ML, which has a lot of safety programming done
in it if you find this appealing.
Here's a quote from Robin Miler about ML which I would hope applies
to the future of XML-oriented programming languages
"Most large computer programs are never completely understood; if they
were, they wouldn't go wrong so often and we would be able to describe
what they do in a scientific way. A good language should help to improve
this state of affairs.
There are many ways of trying to understand programs. People often rely
too much on one way, which is called "debugging" and consists of running a
partly-understood program to see if it does what you expected. Another
way, which ML advocates, is to install some means of understanding in the
very programs themselves.
Standard ML was designed with this in mind. There are two particular
ways-of-understanding built in to Standard ML; one is types for
understanding data, the other is the module system for understanding the
structure of the large-scale programs. People who program in a language
with a strong type system, like this one, often say that their programs
have fewer mistakes, and they understand them better. " -- Robin Milner
Happy New Years!
--harry
Harry Halpin
Informatics, University of Edinburgh
http://www.ibiblio.org/hhalpin
|
