Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] meaning of formal specifications

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] meaning of formal specifications


Chronological Thread 
    < Chronological >      < Thread >
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] meaning of formal specifications
  • Date: Tue, 26 Jan 2021 07:11:22 -0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f54.google.com
  • Ironport-phdr: 9a23:ZCbDbxUvHIHDbykghWy9rjkv0z7V8LGtZVwlr6E/grcLSJyIuqrYbReFt8tkgFKBZ4jH8fUM07OQ7/mxHzZdqsrR+DBaKdoQDkBD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs1xxfTvHdFe+tayGxrKFmOmxrw+tq88IRs/ihNuf8t7dJMXbn/c68lUbFWETMqPnwv6sb2rxfDVwyP5nUdUmUSjBVFBhXO4Q/5UJnsrCb0r/Jx1yaGM8L4S7A0Qimi4LxwSBD0kicHNiU2/3/Rh8dtka9UuhOhpxh4w47JfIGYMed1c63Bcd8GQ2dKQ8BcXDFDDIyhdYsCF+UOPehaoIf9qVUArgawCxewC+700DBEmmX70Lcm3+g9EwzL2hErEdIUsHTTqdX4LLsfXvu1zKnJ1jXDb+1Z2TTg44XUdBAuu/eMUq9tesfW00YgDAPFjlSLqYzlITyV1f4BvHKd7+V6U+KglnQrqwBwojizycchkYbJhocPxVDF8SV12po6Jdq9SENiZ9OvDZRfuT2AOYRsXsMiX39nuDw8yrAepZO2fioHxps5yhDRdvGJfYeF7g/tWeuRPDt0mHJrdba8ihu89UWs1+3yW8u13VtIrydJjsXAu38J2hLT6sWLVv1w9Vqv1zaI0gDc8OBEIUYsmKrDMZ4hw7gwmYYNvkTfGS/2nl/6g7GLeUU5/OWj9ufpYq3+q5OCK4N5jhvyP6cul8ClHOg1MwkDU3Kb9Omz0rDo4Ff3T69QjvIsl6nUqJDaKtofpq6+GwJV15ws6xe7Dzu/0dQYmmQLIEtLeB+HgIXlIV7OIPf/Dfewh1Sjji1nyOzBPr3kGpnNL37Dn6n9fbtl9UJQ1A4+wcpc6p9UEL0NPfP+V07ruNHYARI1Kwm0zPzmCNV52IMeQ2WPAqqBPazIqlCI5uMvI/KMZIALuzbxMeIq5/j0gn8/hFARZ6ip3ZoLaHC3BflmLECZbmDtgtcFC2sFog0+TOnyhF2YTTFTf2qyX7475jwjFI2mCp7DSpmxj7yFwSe0BYZbZntGC1CJCXfnbZ+IW/YKaCKII89uiCYIVba7S9xp6Rb7vwjjjrFjM+CcriYfrNfo0MV/z+zVjxA7szJuWZezyWaIGkh+nmITRzI1lIl5qEpxggOK26h5mPxVFppa4fpPXkE7NILT5+N/AtH2HAnGe4HaGx6dXty6DGRpHZoKyNgUbhMlQonwvlX4xyOvRoQtufmTHpVtq/DT2nHwI4B2zHOUjPB83WljedNGMCidvoA69wXXANSUwUCQlqLvdKNFmSCQqCGMym2BuEweWwl1A/2cDCIvI3DOpNG83XvsCrqnCLApKAxEkJfQJa5Da9mvhlJDFq7u


If you put everything in Coq, it makes it harder to see the separation and blurs the lines.

For example, in the case of using Coq & VST (https://vst.cs.princeton.edu/) you have:
- Implementation = your C code
- Formal Specification = your Hoare tripple which also includes the functional definition of the function.
- Contructed proof = the proof of your Hoare triple correctness.


It is not hard to completely separate specs and implementation (I think in all projects I have seen) even when both live in Coq. sometimes, it requires existentially quantifying over the implementation or implementation details.
There is a separate question about "how do we ensure that the spec is correct": that is definitely a philosophical question with no perfect answer.
 

Archive powered by MHonArc 2.6.19+.

Top of Page