Building Software Systems Economically with Mechanized Logic: Initial Design Proposal
Abstract
Our goal is to develop an economical technology for building proved computing systems with mechanized formal logic. The unifying element of this technology is the functional language Rose which we are designing. Rose embodies a powerful formal logic, and it also is an executable, functional programming language. Thus, potentially, Rose provides a single, unified formalism that can express both hardware and software systems and their specifications and requirements. In the long term, with the development of parallel architectures and optimizing compilers that exploit theorem providing, we believe that functional programming languages will be useful across a wide variety of tasks. In the intermediate term, we intend that Rose be convenient for software applications such as encryption boxes, flow modulators, message servers, etc. The purpose of this phase of our work is to mechanize the Rose logic so that it can be used extensively and economically in all of the previous kinds of activities. We will do this by increasing the power of current Boyer-Moore logic and its theorem prover, by defining the Rose language which embodies the expanded logic and presents it in a more conventional and familiar notation, and by implementing a life-cycle support system for Rose that supports the development and maintenance of large collections of Rose functions, theorems, and proofs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 30, 1987
- Accession Number
- ADA188791
Entities
People
- Donald I. Good
- J. S. Moore
- Matt Kaufmann
Organizations
- University of Texas at Austin