One approach to Prof. Hoare's challenge is to view the development of verified software from the perspective of interactive theorem provers. This idea is not new and many medium-scale software systems have been developed and verified in this manner. Developments based on HOL, ACL2, or PVS have already been described and advocated and our position stands on the same line: most powerful (higher-order) theorem proving systems already contain a programming language, programs can be developed and the correctness of these programs can be specified and verified, they can then be compiled into traditional executable code. In this sense, we already have a small scale example of a verification aware programming language. We propose to take advantage of the notion of "dependent types" to ensure that this programming language combines powerful logical capabilities, reasonable expressive power, and practical linkage between computational content and logical annotations.
展开▼
