The features described here are the desired features of a proposed implementation of Higher Order Set Theory.
At present this is totally fantastic, but I hope to be progressing the details of the design alongside prototyping activities, and that should help this to evolve towards the achievable.
The two principle design requirements are that:

The system will be implemented broadly following the LCF paradigm but with some novel features:

Consideration will be given to the ease with which diverse notations can be semantically embedded into HOST. The embedding of SML in the kernel will make this easier because this will make available mutually recursive datatype definitions for abstract syntax. The semantic embedding will also make more convenient definition of semantic functions (using pattern matching) over these syntactic domains. Consideration will also be given to whether special support for languages presented in XML should be provided. 
The primary purpose of the semantic embedding of SML in the kernel is to enable evaluation of functions defined in the object language to be done efficiently during proof.
This will mean that arithmetic computations involving functions defined in the object language using embedded SML will be evaluated, during the course of proofs, as a part of rewriting, without any performance penalty.
Unfortunately, well behaved arithemetic facilities are at present available only for integers. Floating point arithmetic is not suitable for use in this context. A rational arithmetic package is available for CAML, but this still falls short of the needs for a computationally efficient implementation of classical analysis. Such an implementation will be needed before proof based mathematics can displace less rigorous methods as a practical method of solving real engineering problems. 
As indicated above, though the primitive logic is quite simple, the logical kernel is much more complex, incorporating the logic of a large subset of core standard ML.
Getting this (derived) logic right is the main theoretical challenge in this proposal, and may take some time.
Prototyping of the kernel will take place concurrently with this more theoretical work.
At a first cut this is just a problem of devising a routine embedding of a well defined small programming language into higher order set theory, which is rather like a routine rewriting of the semantics (which is currently defined using a structured operational semantics). The benefit from doing this will however be sensitive to how well the embedding is integrated with the rest of the object language. To get a good solution will not be a routine exercise. 
Are Foundations Necessary?  
HOST rationale  HOST pedigree  HOST features 
