Pure intuitionistic higher-order predicate logic
This is what Haskell is. A pure high-order predicate logic compiler.
System-FW (the formal system of logic) on the top, and Lambda Calculus (the minimal pure language to express any computation) on the bottom.
It may be thought the other way around.
two separate DSLs
Actually three.
- a pure-functional meta-language of propositions (types)
- a pure-functional language for proofs (programs)
the third one is a meta-language about types (meta-languages all the way up)
Programs are proofs
- a valid program is a proof (by example) of a set of propositions
- an inductive/recursive proofs are the most common functions
the general form of a proof (program) is to derive a conclusion on the basis of some (or possibly no) assumptions.
the assumptions are symbols bound in the global environment and modules
those are already checked for correctness and represent prior knowledge - statements of fact (constants) and executable algorithms (pure functions)
derivations (programs) are built up inductively (recursively) from smaller ones (function composition).
evaluation (reduction) of expressions (terms) is done mechanically by application of a small set of well-defined dediction (reduction) rules.
See Philosophy/Logic.
