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.

Last modified 13 months ago Last modified on Jan 7, 2020, 12:00:23 PM
Note: See TracWiki for help on using the wiki.