Proofs and development

[Wolfram Kahl]

Alan Grover (awgrover@umich.edu) 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