monad thinking process
Shawn P. Garbett
Shawn@Garbett.org
Fri, 25 Jan 2002 10:46:48 -0600
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
On Friday 25 January 2002 06:14 am, Cagdas Ozgenc wrote:
> Greetings.
>
> I have very little experience with monads. However my first impression is
> that there is too much thinking process involved in programming with
> monads, and it is very time consuming, at least for a beginner like myself.
> I don't know how productivity changes once you get used to programming with
> them. Also, I have serious concerns about the maintenance of programs
> written in monadic style. Since there is too much plannning overhead, it
> doesn't seem suitable for evolutionary software development process.
>
> What do monad experts think? What do you think of code readability? How
> easy is it to prove that programs written with monads are correct? How does
> changing one function affect other functions, in terms of maintenance?
I'm no monad expert, but I do have a strong opinion on this subject. I've
been programming for a living for twelve years now and various solutions have
been proposed over the years to the "Software Crisis". Structured
programming[1] was a start, then onto actually designing things before
building them, code audits, client server, etc. The current round of snake
oils include UML, CMM, and object-oriented programming. These things did and
do help, but the core root underlying problems of software development still
seems to persist. Dijkstra refered to current development methods as
"attempting to discipline the undisciplined."[2] I've been looking for
something to make my means of making a living easier for years.
In a discussion of this Dr. Stacy Prowell, he told me an interesting idea.
Imperative programming creates logical structures that have state, yet none
of the mainstream development methods of software directly address any of the
known mathematical properties of state machines. Sure you can make a
state-diagram, but where is there a consistent mathematical approach to
state-machines in imperative programming? Most beginners are encouraged to
just think about the problem, maybe even do a little design and begin coding.
Dr. Prowell's main research into cleanroom software development[3] is the
opposite of this. Cleanroom is a treatment of software development as a
concise mathematical state box[4].
What's the benefits of the current methods of "Cleanroom" software
development? Reliable well defined software. The space shuttle control code
team uses a variant of cleanroom with an obsessively huge number of code
walkthroughs. The cellular industry uses it to create rock solid reliable
phone switches. Some medical companies are using it to try and prevent
another Therac-25 incident[5]. Even some linux kernel developers apply it to
get rock solid behavior from their hardware drivers. Test cases for a
Cleanroom model are derived in a mathematical way.
What's the problem with it? It's more expensive in time, upfront time costs,
maintenance cost is incredibly reduced and an overall cost savings has been
demonstrated. It's also horribly tedious in addition to not being well
understood or adopted by the mainstream.
I personally have been working on a set of automated tools to take all the
tedium out of the process. I'm quite close to that goal and heading toward
automated code generation.
The state monad is a perfect for application of cleanroom techniques. If one
followed a cleanroom enumeration through to a canonical state box, a state
monad could implement it in a canonical understandable form. The behavior of
that state monad would be mathematically well defined.
Sitting down and writing state monads from scratch just by thinking about it
leads back down the path of the "pitfalls of imperative programming."[6] It's
quite easy to do with a small problem, but the moment you get into a larger
problem--it'll be back to the hack/test cycle. Imperative and state based
programming is necessary for a large number of problems in computer science.
Why not apply computer science to the construction of their solutions? The
use of the Cleanroom model leads mathematically to a canonical construction
of a state monad.
"Evolutionary" doesn't have to mean hack/test. It can be done in a logic
manner. I highly recommend reading the book
_Cleanroom_Software_Engineering_[3]. It's the Cleanroom method covered with a
case walkthrough, without the hardcore math. If you're interested in the
mathmatical reasoning behind the method, then check out Dr. Prowell's
dissertation[4].
>stepping off the soap box<
Shawn Garbett
[1] _Structured_Programming_: R.C. Linger, H.D. Mills, B.I.Witt, 1979,
Addison-Wesley Publishing Company, Inc. This book is one of the early books
that advocates structured programming and many of the practices that were
adopted early in computer science. Cleanroom methodology is a logical
descendent of the math in this book.
[2] Dijkstra's lecture notes
[3] _Cleanroom_Software_Engineering:_Technology_and_Process_, Stacy J.
Prowell, Carmen J. Trammell, Richard C. Linger, Jesse H. Poore,
Addison-Wesley, 1999, ISBN 0-201-854480-5
[4] _Sequence-Based_Software_Specification_(Ph.D. Dissertation), Stacy J
Prowell, University of Tennessee, May 1996.
http://www.cs.utk.edu/sqrl/publications.html
[5] http://courses.cs.vt.edu/~cs3604/lib/Therac_25/Therac_1.html
[6] _Structure_and_Interpretation_of_Computer_Programs_, 2nd edition, Harold
Abelson, Gerald Jay Sussman, Julie Sussman, MIT Press/McGraw-Hill, 1996, pg
234-6.
- --
You're in a maze of twisty little statements, all alike.
Public Key available from http://www.garbett.org/public-key
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.0.6 (GNU/Linux)
Comment: For info see http://www.gnupg.org
iD8DBQE8UYv5DtpPjAQxZ6ARAsmDAJ9kCqNTSZY12fY8L4WP5z6YD8qPjQCfS6VL
udCs4jlc3ppHYSvu/ai22Po=
=1HMT
-----END PGP SIGNATURE-----