From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 136B07FA1F for ; Sat, 12 Jul 2014 13:56:18 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rdicosmo@gmail.com) identity=pra; client-ip=209.85.212.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of rdicosmo@gmail.com designates 209.85.212.172 as permitted sender) identity=mailfrom; client-ip=209.85.212.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f172.google.com) identity=helo; client-ip=209.85.212.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="postmaster@mail-wi0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkUBAHIhwVPRVdSslGdsb2JhbABZg2BTrwKSQohTFg8BAQEBBwsLCRIqhAMBAQEEEigGARQZCwEDDAEFBRgJBCEPBSABBQEBCRgTCQkQiAwDEQQBAwWiI2qQKYtQJwMKhygRAQUOjmWEDIEWBYRrBX6VH4FLjD+EI0GBaoMMaoEC X-IPAS-Result: AkUBAHIhwVPRVdSslGdsb2JhbABZg2BTrwKSQohTFg8BAQEBBwsLCRIqhAMBAQEEEigGARQZCwEDDAEFBRgJBCEPBSABBQEBCRgTCQkQiAwDEQQBAwWiI2qQKYtQJwMKhygRAQUOjmWEDIEWBYRrBX6VH4FLjD+EI0GBaoMMaoEC X-IronPort-AV: E=Sophos;i="5.01,649,1400018400"; d="scan'208";a="71180427" Received: from mail-wi0-f172.google.com ([209.85.212.172]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 12 Jul 2014 13:56:17 +0200 Received: by mail-wi0-f172.google.com with SMTP id n3so456106wiv.11 for ; Sat, 12 Jul 2014 04:56:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; bh=UhsHF/RkiHX1K8S+wyuMEUga19eSXWL9XXKSP1HQclo=; b=DD/FwPeTaDAc6aATRqSI8pZJig6iutB6QwtEKP48BFK2AZJ1BA4NaS0x2/mDgSqSEy KTox3ejQu2HHmrKkljl7HR02PMVtceIUe9+vT36PL4RLI/nedet4n0t9jDFTZ+3U4Sru SWdyxi1lly983S57rl/jxH6ipps/EGuvwE0vzX48e2jJ3hfgB/o8utNTqCipRO64LgEi qeafvOV09OhOxCFiq0PwN9mNYyoW5+xnDC8VenwjYqUoKW88MG8ecFkzibkQVPOhdE9Q Ts8Z4hWL+1fnh+/qZJU8PGDdW2zTvriIkActrMONBREZVPnExMa2ZsxiznvWH1sttYLg KpDw== X-Received: by 10.180.105.170 with SMTP id gn10mr12517564wib.31.1405166177175; Sat, 12 Jul 2014 04:56:17 -0700 (PDT) Received: from traveler (80-110-42-120.static.surfer.at. [80.110.42.120]) by mx.google.com with ESMTPSA id de6sm11384325wjc.16.2014.07.12.04.56.15 for (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 12 Jul 2014 04:56:16 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by traveler with local (Exim 4.82_1-5b7a7c0-XX) (envelope-from ) id 1X5vuY-0002jH-Ov; Sat, 12 Jul 2014 13:56:14 +0200 Date: Sat, 12 Jul 2014 13:56:14 +0200 From: Roberto Di Cosmo To: Oliver Bandel Cc: caml-list@inria.fr Message-ID: <20140712115614.GB10231@traveler> References: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de> User-Agent: Mutt/1.5.23 (2014-03-12) Subject: Re: [Caml-list] Program proof - how to do that? 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