The Irish School of Constructive Mathematics (
M
C
♣
), which extends the VDM, exploits an algebraic notation based upon monoids and their morphisms for the purposes of abstract
modelling. Its method depends upon an operator calculus. The School hereto eschewed every form of formal language and formal
logic, relying solely upon constructive mathematics.
In 1995 the School committed itself to the development of the modelling of (computing) systems in full generality. This was
achieved by embracing Category Theory and by exploring a geometry of formal methods using techniques of fiber bundles. From
fiber bundles to sheaves was a natural step. Concurrently, the School moved from the algebra of monoids to categories, and
from categories to topoi. Finally, the constructive nature of the School is now coming to terms with formalism and logic through
the (natural) intuitionistic logic inherently manifest through topoi.
In this paper we exhibit an accessible bridge from classical formal methods to topos theoretic formal methods in seeking a
unifying theory.
Keywords Cartesian closed category - constructive mathematics - Heyting algebra - intuitionistic logic - modelling - Topos Theory - Unifying Theory - VDM