From: Oliver Bandel <oliver@first.in-berlin.de>
To: caml-list@inria.fr
Subject: [Caml-list] Program proof - how to do that?
Date: Sat, 12 Jul 2014 13:25:48 +0200 [thread overview]
Message-ID: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de> (raw)
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
next reply other threads:[~2014-07-12 11:25 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-07-12 11:25 Oliver Bandel [this message]
2014-07-12 11:56 ` Roberto Di Cosmo
2014-07-12 12:07 ` Gabriel Scherer
2014-07-19 19:18 ` David MENTRÉ
2014-07-21 22:37 ` Oliver Bandel
2014-07-22 8:25 ` Nuno Gaspar
2014-07-22 22:31 ` Oliver Bandel
2014-07-12 12:26 ` John Whitington
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de \
--to=oliver@first.in-berlin.de \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).