From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id 9345A5D4 for ; Mon, 3 Sep 2018 16:03:16 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.53,325,1531778400"; d="scan'208";a="344722628" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 03 Sep 2018 18:03:14 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 94A62824B5; Mon, 3 Sep 2018 18:03:14 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id EC644824B2 for ; Mon, 3 Sep 2018 18:03:08 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=david.mentre@bentobako.org; spf=Pass smtp.mailfrom=david.mentre@bentobako.org; spf=None smtp.helo=postmaster@tempura.bentobako.org IronPort-PHdr: =?us-ascii?q?9a23=3Az/Wasx0/T8bhUXnZsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?se0SIvad9pjvdHbS+e9qxAeQG9mDtLQc06L/iOPJYSQ4+5GPsXQPItRndiQuro?= =?us-ascii?q?EopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZv?= =?us-ascii?q?JuTyB4Xek9m72/q99pHPYQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+?= =?us-ascii?q?VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfM?= =?us-ascii?q?QA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlT?= =?us-ascii?q?kJNzA5/m/UhMJ/gq1UrxC9qBJw2IPUfIKYOeBicq/Bc94XR2xMVdtRWSxbBYO8?= =?us-ascii?q?apMCAeQbMuZGronyukMBoxyxCwe0Gu3h1iNNjWLx0KInyeshDwDG0xE6E9ILrn?= =?us-ascii?q?vUqsn1NL0MXu2u16bH0zPDb+9R2Tjm8ofIcRchreuLXbJqfsrc0E8iHB7GgFWI?= =?us-ascii?q?sYHoOzyY2v4Tv2WV9eZtW+aih3Qmpgx+ujSiwschhpPUio4LyV3I7zh1zYkxKN?= =?us-ascii?q?GiVkJ3fcCoHZ1NvC+ALYR2WNktQ2RwtSY61LIGvZm7cTAWyJs5wh7fc+GHc5KS?= =?us-ascii?q?7R75T+mePzF4hG5ieL2knRmy8k+gxvf7Vsmu31ZGtitFkt/SuXARzxHe7seKRu?= =?us-ascii?q?Fj8kqvwzqC2QTe5vtFLE07jabbLoQuwr80lpodq0TDGSr2lV3rg6CMaEUk+/Wn?= =?us-ascii?q?5/7iYrr4oJ+cK5V0hR/lP6s1hMO/B/g4Mg8VUGeB+uS806fv/UrjQLVFlvE2iL?= =?us-ascii?q?XWsIjGJcQHoa60GxNa3Zwm6xa7Fjum1NUYnWIbLF9eYxKGj43pO0nUL/ziDPe/?= =?us-ascii?q?hU6skDZxyPzcML3hGMaFEn+Wm77kefN56lVA4As119FWoZxOWZ8bJ/emdkbvtd?= =?us-ascii?q?DvKzIfDzYVi7LrAct82sUbVGSTGKKxOq7UrViC7+EoZe6Wa9lG637GN/E56qu2?= =?us-ascii?q?3jcCklgHcPzxhMpFWDWDBv1jZn6hTz/pi9YFH30Nu1NjHubnjkGFWzdQYDC1Ra?= =?us-ascii?q?1uv2hnWrLjNp/KQ8WWuJLExD2yR8AEbG1AFleGGHTvMYKeVKVUMX/AEopaijUB?= =?us-ascii?q?EIOZZcoh2BWp7lSo17diNvfO82sSuJT/09J85OqVkgs9p2R5?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BhCwCXWo1b/0AnF15bH4NggWSEGpRAg?= =?us-ascii?q?WBBkFuHOAsrAYRAAoNHGQcBBDQUAQIBAQIBAQEBAWwogjUigmEGIw8BBVELGgI?= =?us-ascii?q?mAgIfOBMIAQGDHYIGAaN2gS6EbINNgUWBC4EiiCuCF4E5gmuFS4I0glcCm1YHA?= =?us-ascii?q?hqHQ4gWHYFAhw4lhWaTZYFYIYFVfUOCbZBUgWgBAY0YAQE?= X-IPAS-Result: =?us-ascii?q?A0BhCwCXWo1b/0AnF15bH4NggWSEGpRAgWBBkFuHOAsrAYR?= =?us-ascii?q?AAoNHGQcBBDQUAQIBAQIBAQEBAWwogjUigmEGIw8BBVELGgImAgIfOBMIAQGDH?= =?us-ascii?q?YIGAaN2gS6EbINNgUWBC4EiiCuCF4E5gmuFS4I0glcCm1YHAhqHQ4gWHYFAhw4?= =?us-ascii?q?lhWaTZYFYIYFVfUOCbZBUgWgBAY0YAQE?= X-IronPort-AV: E=Sophos;i="5.53,325,1531778400"; d="scan'208";a="344722608" Received: from tempura.bentobako.org ([94.23.39.64]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 03 Sep 2018 18:03:08 +0200 Received: from [10.0.2.15] (unknown [95.128.149.202]) by tempura.bentobako.org (Postfix) with ESMTPSA id E5844930 for ; Mon, 3 Sep 2018 18:03:07 +0200 (CEST) To: caml-list@inria.fr References: <1C15EE94-097B-4758-815F-1F9D0BB5EF6C@ensta.fr> From: =?UTF-8?Q?David_MENTR=c3=89?= Message-ID: <30e39671-f6a3-cbd5-284e-ed23d4456adf@bentobako.org> Date: Mon, 3 Sep 2018 18:02:26 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.9.1 MIME-Version: 1.0 In-Reply-To: <1C15EE94-097B-4758-815F-1F9D0BB5EF6C@ensta.fr> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US Subject: Re: [Caml-list] FoCaLiZe 0.9.2 released Reply-To: =?UTF-8?Q?David_MENTR=c3=89?= X-Loop: caml-list@inria.fr X-Sequence: 17042 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: Hello François Pessaux, Le 03/09/2018 à 10:38, François Pessaux a écrit : > The FoCaLiZe system provides means for the developers to formally express > their specifications and to go step by step (in an incremental approach) to > design and implementation, while proving that their implementation > meets its specification or design requirements. The FoCaLiZe language offers > high level mechanisms such as inheritance, late binding, redefinition, > parametrization, etc. Confidence in proofs submitted by developers or > automatically generated ultimately relies on Coq formal proof verification. A maybe naive question: what are the distinguishing points of Focalize compared to Coq, Isabelle, F* or B Method? For which fundamental reason I should use Focalize instead of other tool to develop high integrity programs or systems? I read the "What is it FoCaLiZe ?" section but for me it does not answer my question. You can reply to me privately if you think this is inappropriate for caml-list. Best regards, D. Mentré -- 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