Are proof techniques industrially operational?

This article provides a summary of various experiments in using proof techniques which have been performed at AIRBUS FRANCE. It is shown that the main difficulties in using these techniques are twofold: Difficulties in using related tools themselves such as: domain coverage, scalability, user interface, intrinsic limits, It is a fact that these difficulties are on the way to be solved and one can think that, from that strict point of view, the toolkits will be industrially useable within a couple of years, Difficulties related to methodological aspects: indeed the potential users are far from being familiar with the embedded mathematical concepts anymore, even if they used to be familiar at the beginning of their career, because of their day to day focus on more pragmatic aspects such as servo loop concerns or man machine interface. It seems also very difficult and even impossible, to have teams specialized in using these mathematical methods especially in the field of civil aircraft where one of the keys to success already identified is, for the different teams, their ease to communicate. As a conclusion it is suggested that a wide deployment of such proof techniques, which indeed could decrease the validation costs, would require a large educational programme to enable the actors to use them in their day to day work. It is also suggested that the pure mathematical aspects should be hidden from the user who could use the tools as easily as any other specification means