Alan Grover ([EMAIL PROTECTED]) writes (on the Clean list): > I'd then like to modify the source code adding the better algorithm, but I'd > like to keep the original algorithm as the documentation. The > language/system should then help me prove that the better version is > equivalent. I feel that this helps keep the source code understandable, and > connects it more directly with the requirements and specifications. > > ... > > > This all has relation to literate programming, does anyone else have > interest in that? This kind of approach is big part of the motivation behind my graphically interactive strongly typed term graph program development and transformation system HOPS (work in progress), see URL: http://diogenes.informatik.unibw-muenchen.de:8080/kahl/HOPS/ HOPS in principle is a language-independent term graph programming framework with support for user-defined text generation from term graphs. The only constraint are the kind of term graphs supported (with explicit variable binding and variable identity, and with second-order rewriting) and the typing system (essentially simply-typed lambda-calculus with type variables). HOPS distinguishes - ``declarations'' (type signatures in Haskell) that introduce a new identifier with its typing, and - ``rules'', which are term graph transformation rules normally considered as semantics preserving equations. Rules in a certain shape can be used as definitions in functional programming languages; other rules may serve as theorems or lemmata. The possibility of classifying declarations and rules into groups according to their perceived role is not yet fully implemented; considerable flexibility is needed here since among the many possible definitions: one may be the ``documentation version'', one may be best for this compiler, another may be best for that compiler, yet another may be best as a starting point for transformation into a different paradigm. However, attributes on types (such as uniqueness or Haskell's type classes) are not implemented yet, and currently types are always maximally identified, which is incompatible with unique types. Therefore, the current version of HOPS best supports a Haskellish style of programming, and in the supplied rudimentary standard library only output to Haskell is currently supported (to a certain extent). Wolfram