--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on April 2009 ---
CUOQ Pascal wrote: > Hi Nicolas, > >> Is there a method to verify an axiomatization in an annotated C file ? > > You know, what with automatic theorem provers that are > barely able to prove a couple of simple properties as things stand > on the one hand, and G?del's second incompleteness theorem on > the other hand, I think there is potential for some really good > sarcastic remarks here. > I really wish I knew more about these things. > I'd be cracking jokes... you couldn't stop me. > > More seriously, this reminds me of an interesting discussion > at the training session (well, the beginning of a discussion. > The only bad thing about that day was that it was too short). > If we are going to use first-order logic as an alternative > programming language in which alternative versions of the > C functions are defined and composed... but I am getting > ahead of myself. For those who weren't > there, I should provide context by saying that Virgile took > advantage of his talk to match a sort function and its > specification in real time... > Now, if we are going to use first-order logic as > an alternative programming language, > we will at some point have to make it acceptable > as a programming language. > So the future probably holds a lot of module systems, > syntactic restrictions, static consistency checks,... > But to answer your question, and to the best of my knowledge, > we don't have much of all that for now. I don't understand why you are so pessimistic, Pascal. The answer is simple: just realize your axiomatization in Cuoq. Sorry: I meant in Coq. - Claude