ladkin@kestrel.ARPA (Peter Ladkin) (02/21/86)
Some of the discussion about assembler vs higher-level languages is a little hard to believe. A year ago, I wrote a propositional logic theorem prover in OBJ. It's guaranteed complete and correct, although a little slow. It took me 10 minutes to learn the language and code the equations. Anyone who wishes to save time by rewriting it in DEC10 assembler is welcome to. I have designed a calculus of time intervals, which will form the basis of a time expert for a knowledge-based software engineering environment. The hard part was the mathematics. Since our specification language supports assertional definition of functions (axioms) as well as procedural definition, and supports some finite set theory, it might take me a day to type in the definition of the prototype. Again, anyone who wishes to save time by recoding it in lisp (aka the assembler for the Symbolics) is welcome to. Does anyone want to show me how to save time, and guarantee correctness, by recoding in structured assembler? Peter Ladkin