home | mathematics ::... 1 | 2

I have always felt uneasy with classical mathematics and set theory; meeting Per Martin-Löf and his type theory in 1980 made me realize that it was possible to do mathematics in a more satisfactory way.
Since then, I have been active in the building up of "satisfactory" (which in my view requires: intuitionistic and predicative) mathematics, topology in particular, using Martin-Löf's type theory as a foundation.

When topology is developed in this way, the pointfree approach is fundamental; this is why it is called formal.
Begun in the 80s by myself in collaboration with Martin-Löf, formal topology has grown considerably, both in theoretical understanding (inductive methods in topology, predicative proof of the completeness theorem for intuitionistic logic,...) and in scope (in particular, by the inclusion of domain theory).

The deep motivation for predicativity is that it makes formal topology an ideal tool (perhaps the only one) to connect infinitistic methods in mathematics with the computational content, while keeping them clearly distinct. More on formal topology ::...

Two workshops on Formal Topology have been held, 1WFTop in Padova, October 1997, and 2WFTop in Venice, April 2002. Both have been appreciated for bringing together different approaches to pointfree topology and for their relaxed and constructive atmosphere. The proceedings of 2WFTop will soon appear as a special issue of Annals of Pure and Applied Logic (see the 2WFTop table of contents).
I am now thinking about the 3WFTop: suggestions are welcome.

The experience of developing topology over type theory has brought me to a specific practical attitude on foundations, which I call minimalist, and also on the problem of systematic implementation of mathematics on a computer. To this aim, one needs both a ground intensional type theory (essentially, a programming language) and a stock of high level tools on top of it, or "toolbox", which provide with an extensional framework and standard mathematical notation. To preserve the computational content and systematic formalization, each tool is introduced according to a discipline, which I called the forget-restore principle. More on toolbox and the minimalist attitude ::...

Maths, i.e. the force of (earth's) content. Picture of Vulcano, Sicily