--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on April 2009 ---
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. Pascal