FSMLabs is making its way through the DO178 requirements and we’ve given a lot of thought to Common Criteria over the last couple years. One of the advantages of DO178 is that it does not accept the totally untested and frankly unlikely premises of “formal methods”.
The reason mathematics has advanced so much was not because of the Euclidean axioms-lemma-theorem straitjacket, but in spite of it. Luckily, when we actually discover mathematics, we do it the Babylonian way, empirically and algorithmically. It is only when it is time to present it, that we put on the stifling Greek formal attire.
so says Doron Zeilberger
And the mystery quote. Who said this?
“That mathematics reduces in principle to formal proofs is a shaky idea” peculiar to this [20th] century. In practice, mathematicians prove theorems in a social context. […] It is a socially conditioned body of knowledge and techniques.”