Loading ...
Sorry, an error occurred while loading the content.

Re: Does OCaml need proofs?

Expand Messages
  • Christopher Conway
    ... theorem-proved to be sure it does what it is intended. ... translates OCaml code into Coq s input or other theorem provers? If you want to prove a theorem
    Message 1 of 18 , Feb 19, 2009
    • 0 Attachment
      --- In ocaml_beginners@yahoogroups.com, silviu andrica
      <silviu_andrica@...> wrote:
      > I was wondering if a program written in OCaml needs to be
      theorem-proved to be sure it does what it is intended.
      > I mean, is there a theorem prover for OCaml, or a tool that
      translates OCaml code into Coq's input or other theorem provers?

      If you want to prove a theorem about the program which is stronger
      than the theorems you get "for free" from the type checker [1] (e.g.,
      termination, race- and deadlock-freedom) then yes, of course you need
      a separate theorem proving tool. I'm not aware of any such tool for
      OCaml programs. (As others have pointed out, Coq goes in the opposite
      direction: proofs to programs, not programs to proofs.)

      Regards,
      Chris

      [1][http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps Philip
      Wadler. Theorems for free!]
    • Jon Harrop
      ... I d be interested to know what the bugs were... -- Dr Jon Harrop, Flying Frog Consultancy Ltd. http://www.ffconsultancy.com/?e
      Message 2 of 18 , Feb 19, 2009
      • 0 Attachment
        On Thursday 19 February 2009 14:56:41 Richard Jones wrote:
        > There's also a good paper where the authors translated the OCaml
        > stdlib Map module by hand into Coq, proved it, then automatically
        > extracted the code back to OCaml. (And found a bug or two along the
        > way). Unfortunately I can't find that paper right now.

        I'd be interested to know what the bugs were...

        --
        Dr Jon Harrop, Flying Frog Consultancy Ltd.
        http://www.ffconsultancy.com/?e
      • Mehdi Dogguy
        ... Actually, It was in the Set module. The paper can be found here: Functors for Proofs and Programs (J.-C. Filliâtre and P. Letouzey)
        Message 3 of 18 , Feb 19, 2009
        • 0 Attachment
          Richard Jones wrote:
          >
          > There's also a good paper where the authors translated the OCaml
          > stdlib Map module by hand into Coq, proved it, then automatically
          > extracted the code back to OCaml. (And found a bug or two along the
          > way). Unfortunately I can't find that paper right now.
          >

          Actually, It was in the Set module.
          The paper can be found here:

          Functors for Proofs and Programs
          (J.-C. Filliâtre and P. Letouzey)
          http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz

          --
          Mehdi Dogguy مهدي الدقي
          http://www.pps.jussieu.fr/~dogguy
          Tel.: (+33).1.44.27.28.38
        • Stefano Zacchiroli
          ... AVL balancing bugs. Basically what they proved (IIRC the author of the proofs was Jean-Christophe Filliatre) is that the previous implementation did not
          Message 4 of 18 , Feb 19, 2009
          • 0 Attachment
            On Thu, Feb 19, 2009 at 03:59:28PM +0000, Jon Harrop wrote:
            > I'd be interested to know what the bugs were...

            AVL balancing bugs. Basically what they proved (IIRC the author of the
            proofs was Jean-Christophe Filliatre) is that the previous
            implementation did not guarantee maximal balancing at any specific
            time in the internal data structure.

            Out of memory, I don't think there is a paper, but more likely a
            contrib entry in the Coq library.

            Cheers.

            --
            Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
            zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
            Dietro un grande uomo c'è ..| . |. Et ne m'en veux pas si je te tutoie
            sempre uno zaino ...........| ..: |.... Je dis tu à tous ceux que j'aime
          • Jon Harrop
            ... Hmm, it only says two internal functions were producing incorrectly balanced trees but not what the exact mistakes were in the source code... :-( -- Dr
            Message 5 of 18 , Feb 19, 2009
            • 0 Attachment
              On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
              > Richard Jones wrote:
              > > There's also a good paper where the authors translated the OCaml
              > > stdlib Map module by hand into Coq, proved it, then automatically
              > > extracted the code back to OCaml. (And found a bug or two along the
              > > way). Unfortunately I can't find that paper right now.
              >
              > Actually, It was in the Set module.
              > The paper can be found here:
              >
              > Functors for Proofs and Programs
              > (J.-C. Filliâtre and P. Letouzey)
              > http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz

              Hmm, it only says "two internal functions were producing incorrectly balanced
              trees" but not what the exact mistakes were in the source code... :-(

              --
              Dr Jon Harrop, Flying Frog Consultancy Ltd.
              http://www.ffconsultancy.com/?e
            • François Puitg
              ... The Why tool [1], developed by Jean-Christophe Filliâtre, produces « verification conditions » from annotated Ocaml code. Then , it sends them to
              Message 6 of 18 , Feb 19, 2009
              • 0 Attachment
                De Christopher Conway (19 February, 15:47) :

                > --- In ocaml_beginners@yahoogroups.com, silviu andrica
                > <silviu_andrica@...> wrote:
                > > I was wondering if a program written in OCaml needs to be
                > theorem-proved to be sure it does what it is intended.
                > > I mean, is there a theorem prover for OCaml, or a tool that
                > translates OCaml code into Coq's input or other theorem provers?
                >
                > If you want to prove a theorem about the program which is stronger
                > than the theorems you get "for free" from the type checker [1] (e.g.,
                > termination, race- and deadlock-freedom) then yes, of course you need
                > a separate theorem proving tool. I'm not aware of any such tool for
                > OCaml programs. (As others have pointed out, Coq goes in the opposite
                > direction: proofs to programs, not programs to proofs.)

                The Why tool [1], developed by Jean-Christophe Filliâtre, produces «
                verification conditions » from annotated Ocaml code. Then , it sends
                them to external provers (Coq, PVS, ...) and decision procedures
                (Simplify, ...). Most of the time, human interaction is necessary to
                complete the proofs.

                [1] http://why.lri.fr/index.en.html


                >
                > Regards,
                > Chris
                >
                > [1][http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps Philip
                > Wadler. Theorems for free!]
                >
                >
                >
                >
                > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
                > <html>
                > <head>
                > </head>
                >
                >
                >
                >
                > <body style="background-color: #ffffff;">
                >
                > <!--~-|**|PrettyHtmlStartT|**|-~-->
                > <div id="ygrp-mlmsg" style="width:655px; position:relative;">
                > <div id="ygrp-msg" style="width: 470px; margin:0; padding:0 25px 0 0; float:left; z-index:1;">
                > <!--~-|**|PrettyHtmlEndT|**|-~-->
                >
                > <div id="ygrp-text">
                > <p>--- In <a href="mailto:ocaml_beginners%40yahoogroups.com">ocaml_beginners@<wbr>yahoogroups.<wbr>com</a>, silviu andrica<br>
                > <silviu_andrica@<wbr>...> wrote:<br>
                > > I was wondering if a program written in OCaml needs to be<br>
                > theorem-proved to be sure it does what it is intended.<br>
                > > I mean, is there a theorem prover for OCaml, or a tool that<br>
                > translates OCaml code into Coq's input or other theorem provers?<br>
                > <br>
                > If you want to prove a theorem about the program which is stronger<br>
                > than the theorems you get "for free" from the type checker [1] (e.g.,<br>
                > termination, race- and deadlock-freedom) then yes, of course you need<br>
                > a separate theorem proving tool. I'm not aware of any such tool for<br>
                > OCaml programs. (As others have pointed out, Coq goes in the opposite<br>
                > direction: proofs to programs, not programs to proofs.)<br>
                > <br>
                > Regards,<br>
                > Chris<br>
                > <br>
                > [1][<a href="http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps">http://homepages.<wbr>inf.ed.ac.<wbr>uk/wadler/<wbr>papers/free/<wbr>free.ps</a> Philip<br>
                > Wadler. Theorems for free!]<br>
                > <br>
                > </p>
                >
                >
                > </div>
                >
                > <!--~-|**|PrettyHtmlStart|**|-~-->
                > <div width="1" style="color: white; clear: both;"></div>
                > <!--~-|**|PrettyHtmlEnd|**|-~-->
                > </body>
                > <!--~-|**|PrettyHtmlStart|**|-~-->
                > <head>
                > <style type="text/css">
                > <!--
                > #ygrp-mkp{
                > border: 1px solid #d8d8d8;
                > font-family: Arial;
                > margin: 14px 0px;
                > padding: 0px 14px;
                > }
                > #ygrp-mkp hr{
                > border: 1px solid #d8d8d8;
                > }
                > #ygrp-mkp #hd{
                > color: #628c2a;
                > font-size: 85%;
                > font-weight: bold;
                > line-height: 122%;
                > margin: 10px 0px;
                > }
                > #ygrp-mkp #ads{
                > margin-bottom: 10px;
                > }
                > #ygrp-mkp .ad{
                > padding: 0 0;
                > }
                > #ygrp-mkp .ad a{
                > color: #0000ff;
                > text-decoration: none;
                > }
                > -->
                > </style>
                > </head>
                > <head>
                > <style type="text/css">
                > <!--
                > #ygrp-sponsor #ygrp-lc{
                > font-family: Arial;
                > }
                > #ygrp-sponsor #ygrp-lc #hd{
                > margin: 10px 0px;
                > font-weight: bold;
                > font-size: 78%;
                > line-height: 122%;
                > }
                > #ygrp-sponsor #ygrp-lc .ad{
                > margin-bottom: 10px;
                > padding: 0 0;
                > }
                > -->
                > </style>
                > </head>
                > <head>
                > <style type="text/css">
                > <!--
                > #ygrp-mlmsg {font-size:13px; font-family: arial,helvetica,clean,sans-serif;*font-size:small;*font:x-small;}
                > #ygrp-mlmsg table {font-size:inherit;font:100%;}
                > #ygrp-mlmsg select, input, textarea {font:99% arial,helvetica,clean,sans-serif;}
                > #ygrp-mlmsg pre, code {font:115% monospace;*font-size:100%;}
                > #ygrp-mlmsg * {line-height:1.22em;}
                > #ygrp-text{
                > font-family: Georgia;
                > }
                > #ygrp-text p{
                > margin: 0 0 1em 0;
                > }
                >
                > dd.last p a {
                > font-family: Verdana;
                > font-weight: bold;
                > }
                >
                > #ygrp-vitnav{
                > padding-top: 10px;
                > font-family: Verdana;
                > font-size: 77%;
                > margin: 0;
                > }
                > #ygrp-vitnav a{
                > padding: 0 1px;
                > }
                > #ygrp-mlmsg #logo{
                > padding-bottom: 10px;
                > }
                >
                > #ygrp-reco {
                > margin-bottom: 20px;
                > padding: 0px;
                > }
                > #ygrp-reco #reco-head {
                > font-weight: bold;
                > color: #ff7900;
                > }
                >
                > #reco-category{
                > font-size: 77%;
                > }
                > #reco-desc{
                > font-size: 77%;
                > }
                >
                > #ygrp-vital a{
                > text-decoration: none;
                > }
                >
                > #ygrp-vital a:hover{
                > text-decoration: underline;
                > }
                >
                > #ygrp-sponsor #ov ul{
                > padding: 0 0 0 8px;
                > margin: 0;
                > }
                > #ygrp-sponsor #ov li{
                > list-style-type: square;
                > padding: 6px 0;
                > font-size: 77%;
                > }
                > #ygrp-sponsor #ov li a{
                > text-decoration: none;
                > font-size: 130%;
                > }
                > #ygrp-sponsor #nc{
                > background-color: #eee;
                > margin-bottom: 20px;
                > padding: 0 8px;
                > }
                > #ygrp-sponsor .ad{
                > padding: 8px 0;
                > }
                > #ygrp-sponsor .ad #hd1{
                > font-family: Arial;
                > font-weight: bold;
                > color: #628c2a;
                > font-size: 100%;
                > line-height: 122%;
                > }
                > #ygrp-sponsor .ad a{
                > text-decoration: none;
                > }
                > #ygrp-sponsor .ad a:hover{
                > text-decoration: underline;
                > }
                > #ygrp-sponsor .ad p{
                > margin: 0;
                > }
                > o{font-size: 0; }
                > .MsoNormal{
                > margin: 0 0 0 0;
                > }
                > #ygrp-text tt{
                > font-size: 120%;
                > }
                > blockquote{margin: 0 0 0 4px;}
                > .replbq{margin:4}
                >
                > dd.last p span {
                > margin-right: 10px;
                > font-family: Verdana;
                > font-weight: bold;
                > }
                >
                > dd.last p span.yshortcuts {
                > margin-right: 0;
                > }
                >
                > div.photo-title a,
                > div.photo-title a:active,
                > div.photo-title a:hover,
                > div.photo-title a:visited {
                > text-decoration: none;
                > }
                >
                > div.file-title a,
                > div.file-title a:active,
                > div.file-title a:hover,
                > div.file-title a:visited {
                > text-decoration: none;
                > }
                >
                > #ygrp-msg p {
                > clear: both;
                > padding: 15px 0 3px 0;
                > overflow: hidden;
                > }
                >
                > #ygrp-msg p span {
                > color: #1E66AE;
                > font-weight: bold;
                > }
                >
                > div#ygrp-mlmsg #ygrp-msg p a span.yshortcuts {
                > font-family: Verdana;
                > font-size: 10px;
                > font-weight: normal;
                > }
                >
                > #ygrp-msg p a {
                > font-family: Verdana;
                > font-size: 10px;
                > }
                >
                > #ygrp-mlmsg a {
                > color: #1E66AE;
                > }
                >
                > div.attach-table div div a {
                > text-decoration: none;
                > }
                >
                > div.attach-table {
                > width: 400px;
                > }
                >
                > -->
                > </style>
                > </head>
                > <!--~-|**|PrettyHtmlEnd|**|-~-->
                > </html><!--End group email -->
                >
              • Christopher Conway
                ... (e.g., ... need ... opposite ... I know about Why, and should have mentioned it, but I didn t realize it works on plain-vanilla OCaml code. Is there a tool
                Message 7 of 18 , Feb 19, 2009
                • 0 Attachment
                  --- In ocaml_beginners@yahoogroups.com, "François Puitg"
                  <francois.puitg@...> wrote:
                  >
                  > De Christopher Conway (19 February, 15:47) :
                  >
                  > > --- In ocaml_beginners@yahoogroups.com, silviu andrica
                  > > <silviu_andrica@> wrote:
                  > > > I was wondering if a program written in OCaml needs to be
                  > > theorem-proved to be sure it does what it is intended.
                  > > > I mean, is there a theorem prover for OCaml, or a tool that
                  > > translates OCaml code into Coq's input or other theorem provers?
                  > >
                  > > If you want to prove a theorem about the program which is stronger
                  > > than the theorems you get "for free" from the type checker [1]
                  (e.g.,
                  > > termination, race- and deadlock-freedom) then yes, of course you
                  need
                  > > a separate theorem proving tool. I'm not aware of any such tool for
                  > > OCaml programs. (As others have pointed out, Coq goes in the
                  opposite
                  > > direction: proofs to programs, not programs to proofs.)
                  >
                  > The Why tool [1], developed by Jean-Christophe Filliâtre, produces «
                  > verification conditions » from annotated Ocaml code. Then , it sends
                  > them to external provers (Coq, PVS, ...) and decision procedures
                  > (Simplify, ...). Most of the time, human interaction is necessary to
                  > complete the proofs.
                  >
                  > [1] http://why.lri.fr/index.en.html

                  I know about Why, and should have mentioned it, but I didn't realize
                  it works on plain-vanilla OCaml code. Is there a tool that strips Why
                  annotations from the input and produces an OCaml output parsable by
                  ocamlc?

                  Regards,
                  Chris
                • Johannes Kanig
                  ... This isn t quite right. While Why s syntax is inspired by OCaml s, it really isn t the same language at all. Why doesn t have variant types, objects,
                  Message 8 of 18 , Feb 20, 2009
                  • 0 Attachment
                    On Thu, Feb 19, 2009 at 8:01 PM, Christopher Conway <cconway@...> wrote:
                    > <francois.puitg@...> wrote:
                    >> The Why tool [1], developed by Jean-Christophe Filliâtre, produces «
                    >> verification conditions » from annotated Ocaml code. Then , it sends
                    >> them to external provers (Coq, PVS, ...) and decision procedures
                    >> (Simplify, ...). Most of the time, human interaction is necessary to
                    >> complete the proofs.
                    > I know about Why, and should have mentioned it, but I didn't realize
                    > it works on plain-vanilla OCaml code. Is there a tool that strips Why
                    > annotations from the input and produces an OCaml output parsable by
                    > ocamlc?

                    This isn't quite right. While Why's syntax is inspired by OCaml's, it
                    really isn't the same language at all. Why doesn't have variant types,
                    objects, polymorphic variants, records, modules. It's references are
                    not really first class values. They can't be returned by functions,
                    for example. Also, support for higher-order programs is very limited;
                    you can write them, but not prove them correct.

                    However you can see Why as a (small) subset of OCaml, and there is
                    indeed an option to output OCaml.

                    --
                    Johannes Kanig
                    johannes.kanig@...
                  • Richard Jones
                    ... As you might have gathered I only have a vague memory of this (sets / maps .. whatever!) but IIRC the bugs were fixed. Rich. -- Richard Jones Red Hat
                    Message 9 of 18 , Feb 23, 2009
                    • 0 Attachment
                      On Thu, Feb 19, 2009 at 04:25:57PM +0000, Jon Harrop wrote:
                      > On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
                      > > Richard Jones wrote:
                      > > > There's also a good paper where the authors translated the OCaml
                      > > > stdlib Map module by hand into Coq, proved it, then automatically
                      > > > extracted the code back to OCaml. (And found a bug or two along the
                      > > > way). Unfortunately I can't find that paper right now.
                      > >
                      > > Actually, It was in the Set module.
                      > > The paper can be found here:
                      > >
                      > > Functors for Proofs and Programs
                      > > (J.-C. Filliâtre and P. Letouzey)
                      > > http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz
                      >
                      > Hmm, it only says "two internal functions were producing incorrectly balanced
                      > trees" but not what the exact mistakes were in the source code... :-(

                      As you might have gathered I only have a vague memory of this
                      (sets / maps .. whatever!) but IIRC the bugs were fixed.

                      Rich.

                      --
                      Richard Jones
                      Red Hat
                    • Guillaume Yziquel
                      ... And is there a way to, sort of semi-automatically, get OCaml code, or a subset of the core language, into Coq? All the best, -- Guillaume Yziquel
                      Message 10 of 18 , Feb 23, 2009
                      • 0 Attachment
                        Richard Jones a écrit :
                        > On Thu, Feb 19, 2009 at 04:25:57PM +0000, Jon Harrop wrote:
                        >> On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
                        >>
                        >>> Richard Jones wrote:
                        >>>> There's also a good paper where the authors translated the OCaml
                        >>>> stdlib Map module by hand into Coq, proved it, then automatically
                        >>>> extracted the code back to OCaml. (And found a bug or two along the
                        >>>> way). Unfortunately I can't find that paper right now.

                        And is there a way to, sort of semi-automatically, get OCaml code, or a
                        subset of the core language, into Coq?

                        All the best,

                        --
                        Guillaume Yziquel
                        http://yziquel.homelinux.org/
                      • Richard Jones
                        ... No. I have only a very shallow understanding of this, but I ll speculate anyway: It wouldn t make sense. You write your Coq proof, and from that can
                        Message 11 of 18 , Feb 23, 2009
                        • 0 Attachment
                          On Mon, Feb 23, 2009 at 07:02:56PM +0100, Guillaume Yziquel wrote:
                          > And is there a way to, sort of semi-automatically, get OCaml code, or a
                          > subset of the core language, into Coq?

                          No.

                          I have only a very shallow understanding of this, but I'll speculate
                          anyway: It wouldn't make sense. You write your Coq proof, and from
                          that can generate working OCaml code, which directly and correctly
                          implements the proof. But to go from random OCaml code to ... what?

                          You're probably better off asking someone on the Coq mailing list.

                          Rich.

                          --
                          Richard Jones
                          Red Hat
                        • Guillaume Yziquel
                          ... I half agree with wour wouldn t make sense statement. The Coq to Ocaml is indeed the cleanest path. However, I was thinking of something more like:
                          Message 12 of 18 , Feb 23, 2009
                          • 0 Attachment
                            Richard Jones a écrit :
                            > On Mon, Feb 23, 2009 at 07:02:56PM +0100, Guillaume Yziquel wrote:
                            >> And is there a way to, sort of semi-automatically, get OCaml code, or a
                            >> subset of the core language, into Coq?
                            >
                            > No.
                            >
                            > I have only a very shallow understanding of this, but I'll speculate
                            > anyway: It wouldn't make sense. You write your Coq proof, and from
                            > that can generate working OCaml code, which directly and correctly
                            > implements the proof. But to go from random OCaml code to ... what?

                            I half agree with wour "wouldn't make sense" statement. The Coq to Ocaml
                            is indeed the cleanest path. However, I was thinking of something more like:

                            http://www.cl.cam.ac.uk/~so294/ocaml/

                            You get the ocaml code "somehow" into Coq, and then you'd be busy
                            painfully proving the operational semantics of your code. Of course,
                            it's not as neat as the purely functional Coq -> Ocaml way.

                            But the whole painful thing is that, well, there's nothing automated in
                            such an import to Coq. I just hoped there was...

                            > You're probably better off asking someone on the Coq mailing list.

                            OK. I will. Thanks.

                            > Rich.

                            --
                            Guillaume Yziquel
                            http://yziquel.homelinux.org/
                          • Mehdi Dogguy
                            ... There is also PAF, which is a Proof Assistant for ML Programs Verification. PAF lets you prove directly you OCaml (or a subset) program. It has been proven
                            Message 13 of 18 , Feb 24, 2009
                            • 0 Attachment
                              Guillaume Yziquel a écrit :
                              >
                              > And is there a way to, sort of semi-automatically, get OCaml code, or a
                              > subset of the core language, into Coq?
                              >

                              There is also PAF, which is a Proof Assistant for ML Programs
                              Verification. PAF lets you prove directly you OCaml (or a subset)
                              program. It has been proven to be coherent (hopefully).

                              You can check this article:

                              http://www.springerlink.com/content/u3xtkcwdnh3jcvux/

                              But, for more updated news, you may contact Séverine Maingaud[1] who
                              works on PAF.

                              [1] http://www.pps.jussieu.fr/~maingaud/

                              Hope this helps,

                              --
                              Mehdi Dogguy مهدي الدقي
                              http://www.pps.jussieu.fr/~dogguy
                              Tel.: (+33).1.44.27.28.38
                            Your message has been successfully submitted and would be delivered to recipients shortly.