Lambda the Ultimate

inactiveTopic Mechanizing the Development of Software
started 8/5/2001; 12:13:52 PM - last post 8/9/2001; 1:04:52 PM
Ehud Lamm - Mechanizing the Development of Software  blueArrow
8/5/2001; 12:13:52 PM (reads: 1221, responses: 2)
Mechanizing the Development of Software
This fairly theoretical paper deals with formalizing the relation between specification and implementation. Implementations are the result of refining specifications.

This agrees with my own point of view: reliability oriented programming should be seen as an activity based on transforming specifications into programs. (Flawed specifications should be highlighted by this transformation process, and fixed.) [from a paper in writing]

Posted to Software-Eng by Ehud Lamm on 8/5/01; 12:17:15 PM

jon fernquest - Re: Mechanizing the Development of Software  blueArrow
8/8/2001; 3:40:44 AM (reads: 804, responses: 0)
Using category theory to help write programs is a cool idea, but when I was reading the paper I was continually muttering to myself ...ok now show me some code...some CAML code or Haskell or Scheme code.... show me how to write a program with category theory! (Note: You can supposedly do this in the language "Charity" which I will probably never have the time to learn.)

Code would give me a concrete anchor that I could work backwards from to see how in fact category theory could help me write programs, but alas it doesn't happen, I'm stuck with a spec that maybe I feed into some proprietary code generator.

To quote the paper:

>It is unlikely that a general automated method exists for constructing rungs of the >ladder, since it is here that creative decisions can be made...... >Our goal in Designware is to build an >interface providing the user with various general automated operations and libraries of >standard components. The user applies various operators with the goal of filling out >partial morphisms and specifications until the rung is complete.

Sounds roughly similar to what Alexandrescu is doing with his implementation of design patterns with C++ metaprogramming in "Modern C++ Design: Generic Programming and Design Patterns".

except C++ and GOF are radically popular and category theory is traditionally an abstruse and unapplied branch of mathemetics and Alexandrescu actually does implement design patterns directly in C++ (immediate gratification):

Quoting Hoare [6]: "Category theory is quite the most general and abstract branch of pure mathematics. The corollary of a high degree of generality and abstraction is that the theory gives almost no assistance in solving the more specific problems within any of the subdisciplines to which it applies. It is a tool for the generalist, of little benefit to the practitioner." Hence it will come as no surprise that, for algorithmics too, category is mainly useful for theory development; hardly for individual program derivation.

(From: A Gentle Introduction to Category Theory Maarten M. Fokkinga, available online) (Quoting: C.A.R. Hoare. Notes on an Approach to Category Theory for Computer Scientists. In M. Broy, editor, Constructive Methods in Computing Science, pages 245{305. Interna- tional Summer School directed by F.L. Bauer [et al.], Springer Verlag, 1989. NATO Advanced Science Institute Series (Series F: Computer and System Sciences Vol. 55).) -------------------------------------------------------------------------

Possibly Ridiculous Over-Generalization:

Category theory is to functional programming what 'refactoring' is to object oriented programming?

Categories make functional programs more understandable via mathematical refinement?

"Refactoring" through a refinement of programming style towards readability (kind of like a "Strunk and White" for programming)?

One difference seems to be that "refactoring" codifies existing programming practice with easy to follow rules of thumb and works directly with code. It's not attached to specific black-box proprietary systems like "Specware, Designware, and Planware."


It seems like: The success of Alexandrescu's methods stems from taking ideas from the Lisp world that were stillborn in the AI winter of the early nineties, namely object oriented meta-programming and the meta-object protocol (MOP), grafting it onto the C++ (that since the introduction of templates has been sitting there ready for it) and doing something useful with it: implementing design patterns. Truly "meta" : C++ templates under Alexandrescu's Loki Design Pattern Library under whatever functionality you're implementing with the design pattern (e.g. directory walking, code generation....)

Now if there was a CAML or Oz category theory library and I could use it for meta-programming....let's say stateful folds (catamorphisms) for walking directory trees or XML queries and transformations, but my imagination is running away with me and grey matter + patience = mathematician, both of which I lack....

Ehud Lamm - Re: Mechanizing the Development of Software  blueArrow
8/9/2001; 1:04:52 PM (reads: 761, responses: 0)
show me some code...

I like the fact that definitions like those Container and Partial-Order are so much like code (like generic signature in Ada, for example). The only thing missing in actual code is the axioms - but their importance is not new: it is basically what ADTs are all about.