Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verification of axiomatization


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