[cssohavu] Enabling arbitrary static verification

As the complexity of programs increase, static verification features of a programming language become relatively more important, compared to say code conciseness or code execution speed (at least, constant factors of code execution speed).  It becomes relatively more important for a machine verifier to be able to "understand" the program and verify correctness properties about it.  That computer verifier might become the only entity that understands the entirety of a large program written over a long period of time by many authors.

Rich type systems such as in Haskell are an example of static verification.  For example, it is useful to be able to annotate which code is stateful and what state it is modifying. Haskell monads accomplish such annotation, and the type checker checks that the annotations are correct.

However, Haskell types are not the be-all-end-all of static verification.  In more complicated code, it is easy to want to express and verify properties which cannot be expressed in its type system.

Design a language whose static verification features are user definable and may be arbitrarily complex, keeping pace with the complexity of the program.

(We will probably eventually want to express static verification of the static verification, and so on.  The difficulty of creating a correct program inherently grows faster than linearly with size of the executable part of the program.  Perhaps this will prevent the technological singularity.)

Language features such as polymorphic types or other type extensions would not be hardcoded into the compiler but imported as one of many possible static verification libraries that a program can invoke in the static verification phase of its compilation.  Theorem provers will also likely be useful as libraries.

Lisp syntax looks nice, with its arbitrary extensibility and ability to treat code as data, which is what the static verification code will be doing.