[Caml-list] Program proof - how to do that?

[Caml-list] Program proof - how to do that?

[Oliver Bandel]

Hello,

how can program proof be done in the real world?
What are the theoretical things needed to know?
And how to bring together the theory and the practise?

During the last some months I looked into how mathematical
proof works, and how natural deduction works (also looked at calculus
for natural deduction).

How can this be used in the real world of (OCaml-)programming
to make a proof on the functionality of software?

There seem to be limits coming from the halting problem,
but AFAIK with a reduced set of operations, then in this
limited set of instructions, this problem can be circumvented.
What are the details on this topic? What kind of operations
can be proofed to be safe (doing what is intended),
and which (kind of) operations would not be possible to
become proofed?

Any explanation as well as hints on literature are welcome.

Ciao,
    Oliver

Re: [Caml-list] Program proof - how to do that?

[Roberto Di Cosmo]

Dear Oliver,
     there have been decades of research going on on all this,
and it would be kind of pretentious to try and sum them up
in a few lines here.

Let me offer a suggestion nonetheless: if you happen to be near Vienna in
the very next days, you should definitely go and attend some of the talks that
will take place in the Vienna Summer of Logic 2014 event (http://vsl2014.at/)

There will be tracks on hardware verification, software verification,
theorem proving, logic and all that :-)

--
Roberto


On Sat, Jul 12, 2014 at 01:25:48PM +0200, Oliver Bandel wrote:
> Hello,
> 
> how can program proof be done in the real world?
> What are the theoretical things needed to know?
> And how to bring together the theory and the practise?
> 
> During the last some months I looked into how mathematical
> proof works, and how natural deduction works (also looked at calculus
> for natural deduction).
> 
> How can this be used in the real world of (OCaml-)programming
> to make a proof on the functionality of software?
> 
> There seem to be limits coming from the halting problem,
> but AFAIK with a reduced set of operations, then in this
> limited set of instructions, this problem can be circumvented.
> What are the details on this topic? What kind of operations
> can be proofed to be safe (doing what is intended),
> and which (kind of) operations would not be possible to
> become proofed?
> 
> Any explanation as well as hints on literature are welcome.
> 
> Ciao,
>    Oliver
> 
> 
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

-- 
Roberto Di Cosmo
 
------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto@dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann       
F-75205 Paris Cedex 13   Identica: http://identi.ca/rdicosmo
FRANCE.                  Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
      http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
 
Bureau 3020 (3rd floor)
Batiment Sophie Germain
Avenue de France
Metro Bibliotheque Francois Mitterrand, ligne 14/RER C
-----------------------------------------------------------------
GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3                        

Re: [Caml-list] Program proof - how to do that?

[Gabriel Scherer]

I tried to (partially) answer this question in the following
StackOverflow thread:
  http://stackoverflow.com/questions/12937082/ocaml-used-in-demonstrations



On Sat, Jul 12, 2014 at 1:25 PM, Oliver Bandel
<oliver@first.in-berlin.de> wrote:
> Hello,
>
> how can program proof be done in the real world?
> What are the theoretical things needed to know?
> And how to bring together the theory and the practise?
>
> During the last some months I looked into how mathematical
> proof works, and how natural deduction works (also looked at calculus
> for natural deduction).
>
> How can this be used in the real world of (OCaml-)programming
> to make a proof on the functionality of software?
>
> There seem to be limits coming from the halting problem,
> but AFAIK with a reduced set of operations, then in this
> limited set of instructions, this problem can be circumvented.
> What are the details on this topic? What kind of operations
> can be proofed to be safe (doing what is intended),
> and which (kind of) operations would not be possible to
> become proofed?
>
> Any explanation as well as hints on literature are welcome.
>
> Ciao,
>    Oliver
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] Program proof - how to do that?

[David MENTRÉ]

Hello Gabriel,

2014-07-12 14:07, Gabriel Scherer:
> I tried to (partially) answer this question in the following
> StackOverflow thread:
>    http://stackoverflow.com/questions/12937082/ocaml-used-in-demonstrations


Nice answer.

BTW, regarding Why3 in your answer, the current git version of Why3 
allows to produce OCaml code from a proved WhyML program, thus allowing 
production of certified OCaml code (like with Coq but using Deductive 
Verification approach and automated provers). This is currently Work In 
Progress and actively developed but this feature will be definitely be 
part of the next stable release of Why3 (and you can already play with 
it by compiling the git version).

Best regards,
david

Re: [Caml-list] Program proof - how to do that?

[Oliver Bandel]

Hello,

thanks to all people who answered.

I'm sorry that I can't attend to the logics conference mentioned in on
answer. Maybe next time.

Would be fine if such events could be mentioned on this list.



Zitat von David MENTRÉ <dmentre@linux-france.org> (Sat, 19 Jul 2014  
21:18:04 +0200)

> Hello Gabriel,
>
> 2014-07-12 14:07, Gabriel Scherer:
>> I tried to (partially) answer this question in the following
>> StackOverflow thread:
>>   http://stackoverflow.com/questions/12937082/ocaml-used-in-demonstrations
>
>
> Nice answer.
>
> BTW, regarding Why3 in your answer, the current git version of Why3  
> allows to produce OCaml code from a proved WhyML program,
[...]


I here now do hear the first time about "Why3".

Interesting to see what is available in the area of program proof.

But my question also was about the theoretical background of the proof stuff.

For example in my exploration of logics I came across model theory and
tarski semantics.
Looks interesting to me, something worth exploring in more detail, I think.

Does anybody know more about these topics (theoretically as well as
if this is used in theorem provers)?


Ciao,
    Oliver

Re: [Caml-list] Program proof - how to do that?

[Nuno Gaspar]

[-- Attachment #1: Type: text/plain, Size: 2186 bytes --]

You wanna take a look at Hoare Logic:
http://en.wikipedia.org/wiki/Hoare_logic

Then, you can peek Weakest precondiction calculus:
http://en.wikipedia.org/wiki/Predicate_transformer_semantics

And if you're brave, Separation logic.
http://en.wikipedia.org/wiki/Separation_logic

Oh, and if you still some more spare time: Rely/Guarantee. :)

Hope it helps.





2014-07-22 0:37 GMT+02:00 Oliver Bandel <oliver@first.in-berlin.de>:

> Hello,
>
> thanks to all people who answered.
>
> I'm sorry that I can't attend to the logics conference mentioned in on
> answer. Maybe next time.
>
> Would be fine if such events could be mentioned on this list.
>
>
>
> Zitat von David MENTRÉ <dmentre@linux-france.org> (Sat, 19 Jul 2014
> 21:18:04 +0200)
>
>
>  Hello Gabriel,
>>
>> 2014-07-12 14:07, Gabriel Scherer:
>>
>>> I tried to (partially) answer this question in the following
>>> StackOverflow thread:
>>>   http://stackoverflow.com/questions/12937082/ocaml-used-
>>> in-demonstrations
>>>
>>
>>
>> Nice answer.
>>
>> BTW, regarding Why3 in your answer, the current git version of Why3
>> allows to produce OCaml code from a proved WhyML program,
>>
> [...]
>
>
> I here now do hear the first time about "Why3".
>
> Interesting to see what is available in the area of program proof.
>
> But my question also was about the theoretical background of the proof
> stuff.
>
> For example in my exploration of logics I came across model theory and
> tarski semantics.
> Looks interesting to me, something worth exploring in more detail, I think.
>
> Does anybody know more about these topics (theoretically as well as
> if this is used in theorem provers)?
>
>
> Ciao,
>    Oliver
>
>
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>



-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible
life choice.

[-- Attachment #2: Type: text/html, Size: 3691 bytes --]

Re: [Caml-list] Program proof - how to do that?

[Oliver Bandel]

Hello Nuno,


many, many thanks, these three are very good hints!


Best Regards,
    Oliver



Zitat von Nuno Gaspar <nmpgaspar@gmail.com> (Tue, 22 Jul 2014 10:25:55 +0200)

> You wanna take a look at Hoare Logic:
> http://en.wikipedia.org/wiki/Hoare_logic
>
> Then, you can peek Weakest precondiction calculus:
> http://en.wikipedia.org/wiki/Predicate_transformer_semantics
>
> And if you're brave, Separation logic.
> http://en.wikipedia.org/wiki/Separation_logic
>
> Oh, and if you still some more spare time: Rely/Guarantee. :)
>
> Hope it helps.
>
>
>
>
>
> 2014-07-22 0:37 GMT+02:00 Oliver Bandel <oliver@first.in-berlin.de>:
>
>> Hello,
>>
>> thanks to all people who answered.
>>
>> I'm sorry that I can't attend to the logics conference mentioned in on
>> answer. Maybe next time.
>>
>> Would be fine if such events could be mentioned on this list.
>>
>>
>>
>> Zitat von David MENTRÉ <dmentre@linux-france.org> (Sat, 19 Jul 2014
>> 21:18:04 +0200)
>>
>>
>>  Hello Gabriel,
>>>
>>> 2014-07-12 14:07, Gabriel Scherer:
>>>
>>>> I tried to (partially) answer this question in the following
>>>> StackOverflow thread:
>>>>   http://stackoverflow.com/questions/12937082/ocaml-used-
>>>> in-demonstrations
>>>>
>>>
>>>
>>> Nice answer.
>>>
>>> BTW, regarding Why3 in your answer, the current git version of Why3
>>> allows to produce OCaml code from a proved WhyML program,
>>>
>> [...]
>>
>>
>> I here now do hear the first time about "Why3".
>>
>> Interesting to see what is available in the area of program proof.
>>
>> But my question also was about the theoretical background of the proof
>> stuff.
>>
>> For example in my exploration of logics I came across model theory and
>> tarski semantics.
>> Looks interesting to me, something worth exploring in more detail, I think.
>>
>> Does anybody know more about these topics (theoretically as well as
>> if this is used in theorem provers)?
>>
>>
>> Ciao,
>>    Oliver
>>
>>
>>
>>
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>>
>
>
>
> --
> Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
> dollars last year.
> Marge: Bart! Don't make fun of grad students, they just made a terrible
> life choice.
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] Program proof - how to do that?

[John Whitington]

Hi,

Oliver Bandel wrote:
> Hello,
>
> how can program proof be done in the real world?
> What are the theoretical things needed to know?
> And how to bring together the theory and the practise?
>
> During the last some months I looked into how mathematical
> proof works, and how natural deduction works (also looked at calculus
> for natural deduction).
>
> How can this be used in the real world of (OCaml-)programming
> to make a proof on the functionality of software?
>
> There seem to be limits coming from the halting problem,
> but AFAIK with a reduced set of operations, then in this
> limited set of instructions, this problem can be circumvented.
> What are the details on this topic? What kind of operations
> can be proofed to be safe (doing what is intended),
> and which (kind of) operations would not be possible to
> become proofed?
>
> Any explanation as well as hints on literature are welcome.

Chapter 6 ("Reasoning About Functional Programs"), of Paulson's "ML for 
the Working Programmer", is a very gentle introduction to this kind of 
thing.

Thanks,

-- 
John Whitington
Director, Coherent Graphics Ltd
http://www.coherentpdf.com/