Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 20 Jun 1994 10:28:59 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA23712;
          Mon, 20 Jun 1994 03:26:32 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA23708;
          Mon, 20 Jun 1994 03:25:52 -0600
Received: from i80fs2.ira.uka.de by irafs1 with SMTP (PP);
          Mon, 20 Jun 1994 11:18:52 +0200
Received: from ira.uka.de by i80fs2.ira.uka.de id <14770-0@i80fs2.ira.uka.de>;
          Mon, 20 Jun 1994 11:25:38 +0200
Date: Mon, 20 Jun 94 11:25:37 EDT
From: reetz <reetz@ira.uka.de>
To: hol2000@leopard.cs.byu.edu
Subject: Program Dokumentation
Message-Id: <"i80fs2.ira.772:20.05.94.09.25.44"@ira.uka.de>

Konrad (konrad@dcs.gla.ac.uk) writes:
>Question: should the source code to HOL2000 be browsable with mosaic? I
>imagine that putting all the links in would be a lot of work, but then
>again, many users seem to end up perusing the sources (to track down
>bugs, reuse code, etc.)

I think this points to a even broader question:
should HOL2000 be made by the use of modern software engineering, e.g.

- COMPLETE documentation of the source code: description of
  all data structures, algorithms, functions, module interfaces

- COMPLETE documentation of the user interface

- programer's style guide line on how to extend HOL2000 using a
  certain, ``clean'' and uniform programing style

- courses and exercises on how to use and extend HOL2000

- strict revision control

- as independent as possible from certain non-standard features of
  a certain implementation of the used programming language

- graphical standard user interface

and so on.

For a lot of ``academic'' software, this is IMHO terrific due to
the resources needed to match it. It would be nice have a software
meeting all that goals, of course...

 
Ralf.

(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                            SFB 358 of the german research     *)
(*  reetz@informatik.uni-karlsruhe.de     society (DFG)                      *)
(*  reetz@ira.uka.de                      University of Karlsruhe, Germany   *)
(*                                                                           *)
(*                "we prove around in a ring and suppose,                    *)
(*                 the goal sits right in the middle and knows."             *)
(*                                                                           *)
(*****************************************************************************)