Fiction, in the tradition of Stanislaw Lem's reviews of imaginary books .
Till the early half of the 21st century, we were building type theories
built with algebraic substrates. This made them excellent for reasoning
about A = B, but lousy for reasoning with forall epsilon > 0, |A - B| < epsilon.
The breakthrough came with three crucial, intertwined insights:
- We should build logics of relations , not functions .
- To compute with relations, we should use prolog -like languages, where computations are non-deterministic, and whose computational content is about relations.
- Relations power order theory, which powers topology. Once topology comes online, we have the world. Computation follows from denotation.
This new breed of languages begin with a theory built of first order logic and order theory , contrasting the Calculus of constructions , which begins with first-order logic with equality . One quickly builds up topology from this, either ala Scott , or via Locales .
Working topologically, we forgo the notion of equality for the notion of
limits. We never state that x = y. Rather, we state that for any sequence of
radii epsilon_i, we will always have that |x - y| < epsilon_i, where the
partial order < is a primitive of our logic. This is of course, horrid for
algebra. The upshot is that we can do analysis.
We discover that programming language semantics, which is really the study of computability, which is really topology, works out beautifully in this setting, as first discovered by Scott and Stratchey , later vigorously expanded under the cumbersome title of synthetic topology of data types and classical spaces . Cumbersome proofs of program properties are the exception, rather than the norm.