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; Fri, 17 Mar 1995 18:59:58 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA174546482; Fri, 17 Mar 1995 11:54:42 -0700 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA174486481; Fri, 17 Mar 1995 11:54:41 -0700 From: Paul "E." Black Received: by jaguar.cs.byu.edu (1.37.109.15/CS-Client) id AA087046529; Fri, 17 Mar 1995 11:55:29 -0700 Date: Fri, 17 Mar 1995 11:55:29 -0700 Message-Id: <199503171855.AA087046529@jaguar.cs.byu.edu> To: hol2000@leopard.cs.byu.edu Subject: where's parallel HOL? I believe that future computers will be dozens or hundreds of CPUs working together. I further believe that one must write code with a parallel architecture in mind to get significant speed-ups: compilers will never be able to find significant parallelism in existing code. Finally formal verification needs all the compute power available. Therefore ... HOL 2000 should be a parallel/distributed implementation. Who's working on a parallel version of *ML, etc.? -paul-