Writing a text which could reasonably be considered as a MAP manifesto is an interesting subject by itself. This is only a pre-first tentative draft.
The title of the Dagstuhl meeting was "Verification and Constructive Algebra", and it is amusing to note that the intersection, from the strict point of view of words, between this title and MAP is empty. Which was striking at Dagstuhl was on one hand the plurality of subjects studied by the participants and on the other hand a deep and subtle unity of *style* in the very nature of the various breakthroughs which were reported.
It is suspected that the order of the letters M-A-P is only due to the general rule applied when acronyms are looked for: trying to find a word meaning something. Nevertheless the word "Mathematics" is probably more *generic*, only in a vague sense, than both others. It can be reasonably considered that algorithms and proofs are some components of mathematics. So that the members of the MAP club are firstly *mathematicians*.
However one of the major results obtained by Hilbert creating the axiomatic organization of mathematics is that in a sense the process can be reversed. The whole domain of mathematics might be formalized, and such an organization amounts on the contrary to consider that algorithmic and logic constitute more primitive subjects than mathematics. This amazing duality is now well known by the lucid mathematicians, and certainly the Dagsuhl participants were of this sort.
Maybe the common kernel of the Dagstuhl participants' style is precisely that they are much more than ordinary mathematicians aware of the fantastic richness of the various interconnections between those three subjects, mathematics, algorithms and proofs, and they hope -- and obtain -- new insights into these domains by studying more carefully, more deeply these interconnections.
Standard mathematics can sometimes be used to deduce from some computing results new mathematical results. This often amounts to produce a certificate for an algorithm, transforming a computing result into a mathematical proof of a result produced by a computer. After all, this could be modelized as a... mapping M + A -> P. The four colours theorem has be obtained in this way.
Other times, mathematics or more precisely logic can be used to produce proofs *and* algorithms extracted from proofs. M -> P -> A. The whole field covered by constructive mathematics can be described in this way. The constructive point of view sometimes leads to new perspectives in some quite "classical" theories, leading to original methods, frequently easier to be understood, simply because they are closer to the material truth; quickly giving efficient algorithms; it's a case of a map M -> A. But when the algorithms begin to give new results, it is important to prove them to certify the results so obtained; in other words M -> A must be completed in M -> A + P.
And so on. This presentation is somehow superficial and more serious constructions modelizing and/or formalizing the various interconnections between mathematics, algorithms and proofs are the heart of the numberous books following the wonderful work about fundamental mathematics due to Hilbert, Brouwer, Gödel, Heyting, Church, Turing, Markov, Post and so many others.
More concretely, the MAP club intends to put together various means which could help to organize more systematically meetings about these questions. The participants are expected to be on watch to detect every organization which might be used from this point of view. The European financial sources must in particular be seriously studied.
This manifesto (due to Francis Sergeraert) is still work in progress. We're waiting for comments on the MAP mailing list.