Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 21 Jun 1994 20:22:04 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12457; Tue, 21 Jun 1994 13:20:51 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA12453; Tue, 21 Jun 1994 13:20:47 -0600 Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk with LOCAL SMTP (PP) id <19025-0@goggins.dcs.gla.ac.uk>; Tue, 21 Jun 1994 20:18:43 +0100 Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA02174; Tue, 21 Jun 94 20:18:40 BST From: tfm@dcs.gla.ac.uk Message-Id: <9406211918.AA02174@switha.dcs.gla.ac.uk> To: reetz Cc: hol2000@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Academic software (was : Program Dokumentation) In-Reply-To: Your message of "Mon, 20 Jun 94 11:25:37 EDT." <"i80fs2.ira.772:20.05.94.09.25.44"@ira.uka.de> Date: Tue, 21 Jun 94 20:18:39 +0100 Ralf Reetz writes: > I think this points to a even broader question: > should HOL2000 be made by the use of modern software engineering, e.g. > ... > and so on. The items in Ralf's message are (mostly) all obviously desirable. However, many of them entail work which, from an academic *RESEARCH* point of view, is not worth doing. The problem is that many of the activities leading to production-quality systems are not of the kind that will gain any university researcher a Ph.D., tenure, publications, etc. It seems therefore crucial to get non-research funding to support these activities. Tom