" People Disliked It " (extract from From Z to B and then Event-B: Assigning Proofs to Meaningful Programs)
Abrial, JR. (2013). From Z to B and then Event-B: Assigning Proofs to Meaningful Programs. In: Johnsen, E.B., Petre, L. (eds) Integrated Formal Methods. IFM 2013. Lecture Notes in Computer Science, vol 7940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38613-8_1
When writing the first paper on Z and starting to spread the idea of using a settheoretic
notation to write a specification before writing a program, I received
sometimes very negative answers. Some days at that time, I was invited to give
a series of lectures at a Summer School but when the organizers saw the subject
of my presentation, they canceled my visit, telling me that this subject was not
relevant to computer scientists.
I discovered then that set theory had a bad reputation among computer scientists
in Academia. I think the reason is that people are very afraid by the formal
definition of it in, say, Zermelo-Fraenkel axiomatization (I agree). Quite often,
computer science academic people confuses mathematics and computation, although
in many working programs recursive and inductive definitions are totally
absent.
On the one hand, computer scientists prefer to use predicate calculus only
in specifications. But in doing that they still quite often confuse predicates (a
logical concept) and boolean expressions (a programming concept). People think
that mathematics has a semantics. Programming languages have of course a semantics, because programs can be executed. But mathematics has no semantics
because it is not executed, it is only used to support modeling and proofs in
various other disciplines (computer science is one of them).
On the other hand, I also noticed during this time, that professional mathematicians
are not good at logic. To figure that out, it is very instructive to see
how the “Intermediate Value Theorem” (a special case of it was proposed by
Bolzano in1817) is “proved” in textbooks. The apparent difficulty comes from
the fact that in this proof one needs to use the completeness axiom of real numbers
and also the classical definition of the continuity of a real function. Both
this theorem and this definition are formally defined by some heavy predicates
involving both universal and existential quantifications. The proofs of the “Intermediate
Value Theorem” that can be seen in the literature clearly show that
their authors do not master predicate calculus: obscure wordings replace clear
treatments. However, it is not at all difficult to have a perfect and readable proof
provided it is made by someone who is “fluent” in first-order predicate calculus.
So, I was clearly in a bad situation: I wanted to reconcile computer scientists
and mathematicians but, apparently, these two communities do not understand
each other very well.
Comments
Post a Comment