I ougth to agree with out in many aspects. But probably the sense of
this thread has been lost.
Although ACM said is nearly impossible to write correct software, i
have a very good experience write them. Yes, i don't strictly formaly
speaking, no formal systems that axiomize counting is complete. So,
even engineer have no FORMAL method to garantee a building won't
follow. Neverthless there plenty of them very confident on the result
of their work. I believe i prior exposure to Kurt Godel would clarify
that.
Anyhow. What you said about large project i agree with. But i am in
the arena of writing very specific tools, like my version of database
competitor for BDB, My kerberos implementation, my telnet server, my
NIS project, and the like. I am writing them alone, i am confident
enough for such. I do not write down my specification in a strictly
formal manner, but i have formal perspective in mind. And that, dude,
that makes a real difference.
I have some already done tools i have been using in stressing
environment. They works like pretty well, no downtime, no performance
bottleneck that could not be achieved before by similar software ...
I think you are right, these method does not scale well. The more the
number of fellows in any given software the lower its quality, at
least that's my experience.
But i have seen large project that are gide by people that have no
ideia about what they were doing. Much of the problems that put even
higher pressure on release dates was because of software per se, but
because of incompetence. That leads to higher and higher increase in
software complexity. since nobody really know what to do, they fired
everywhere and after started working to cure the bullets damage
(remenber, bullets theyselfs shot). Funny, isn't it?
I believe i am coherent, all i can say is that they works for me
alone, because i use them. The results of such approach may be seen by
the users of my software. Whether they works for large team project or
not, i don't know. At least i hope when you say they don't, this may
be justified by your own experience trying to use them, and if it did
not work you are supposed to be sure it was a faulty of the method
itself and no other variable like, incompetent developers, no
familiarity with that method, and the like.
Just my two cents.
On 5/5/05, Valdis.Kletnieks@vt.edu <Valdis.Kletnieks@vt.edu> wrote:
On Thu, 05 May 2005 13:54:57 -0300, Gustavo Rios said:
Altough is very hard to be 100% rigorous, they all - no exception - helps a
lot.
For those interested in doing serious secure programming, i am
confident to suggest them, if you would allow.
Important to know these books is all about about programming, not
about coding, i.e., no particular language syntax is taken into place.
The single biggest problem with all these "rigorous development" disciplines
is that they *are* very hard. And this runs into two different yet related
problems:
1) Doing a rigorous formal analysis of a program like TeX, which is merely
huge but comprised of merely sequential processing, is bad enough. Trying
to do a formal analysis of the things that *need* it (for instance, the Linux
kernel, the Firefox browser) quickly becomes very intractable, as there's all
these nasty timeouts and race conditions and locking issues on SMP machines
and even having to deal with hardware errors...
Did I mention device drivers for poorly or even erroneously documented
hardware, where you're writing formally correct code to totally borked
specifications, which will never actually function because the hardware
has different ideas? (There's 4 errata in the x86 family that are
severe enough that Linux even lists in /proc/cpuinfo whether your
processor is prone to it, and the work-around deployed: fdiv_bug,
hlt_bug, f00f_bug, and coma_bug). And we'll overlook what happens to
rigorously proven numerical algorithms when run on a Pentium chip that
has the rounding issues....
It's also infamously difficult to ensure that you're not writing to a
specification that, while correct, does something totally stupid. For
instance, consider this infamous "thinko" at Hotmail/Passport:
http://www.derkeiler.com/Mailing-Lists/VulnWatch/2003-05/0010.html
You read it, and you hit your forehead with your hand and do a Homeresque
"D'Oh!". But then you realize that this was obviously *not* something
they had thought of testing - which meant it almost certainly wasn't in
the design spec either. So no amount of formal analysis will detect the
proper implementation of a broken design...
PS: As soon as i have some result to show, i may post a url for those
to play with my software.
Exactly. This brings me to:
2) This may work for small single-person efforts. It's generally considered
unacceptable for large projects, which tend to have these ugly issues called
"target release dates".....
Other than those issues, it's a great idea. ;)
