From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA15848; Fri, 1 Oct 2004 11:04:52 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA17904 for ; Fri, 1 Oct 2004 11:04:51 +0200 (MET DST) Received: from mail.dcs.qmul.ac.uk (vicar.dcs.qmul.ac.uk [138.37.95.146]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i9194o4w005811 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 1 Oct 2004 11:04:51 +0200 Received: from xenografia.plus.com ([212.159.85.26] helo=[192.168.7.2]) by mail.dcs.qmul.ac.uk with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.42) id 1CDJLM-0005hK-L3; Fri, 01 Oct 2004 10:04:49 +0100 Message-ID: <415D1D8C.2020802@dcs.qmul.ac.uk> Date: Fri, 01 Oct 2004 10:04:12 +0100 From: Martin Berger User-Agent: Mozilla Thunderbird 0.6 (X11/20040519) X-Accept-Language: en-us, en MIME-Version: 1.0 To: Jean-Christophe Filliatre CC: caml-list@inria.fr Subject: Re: [Caml-list] Formal Methods References: <959E4FC0-12F8-11D9-A9B7-000A95C19BAA@Avisere.com> <16733.2280.350656.716714@gargle.gargle.HOWL> In-Reply-To: <16733.2280.350656.716714@gargle.gargle.HOWL> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-DCS-Interface-Port: 465 X-DCS-Auth-User: martinb X-DCS-clamav-result: clean (1CDJLM-0005hK-L3) X-DCS-uvscan-result: clean (1CDJLM-0005hK-L3) X-Miltered: at concorde with ID 415D1DB2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 higher-order:01 04.:98 side-effects:02 icfp:03 functional:06 polymorphism:06 mixed:07 www:91 www:91 consider:09 pipeline:09 language:10 dcs:11 actually:11 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > The real difficulties in proving functional code appear when > side-effects are mixed with powerful features such as polymorphism or > higher-order. Then it becomes very hard to reason about programs. > Actually, we don't even have a specification language to write > programs properties to be proved. There is a nice challenge for > research here. this has changed recently. please consider http://www.doc.ic.ac.uk/~yoshida/paper/PA.ps http://www.doc.ic.ac.uk/~yoshida/paper/polyrec.ps http://www.doc.ic.ac.uk/~yoshida/paper/icfp04.ps more along those lines is in the pipeline. martin ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners