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 ESMTP id 52F985D4 for ; Mon, 3 Sep 2018 17:07:43 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.53,325,1531778400"; d="scan'208";a="344728657" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 03 Sep 2018 19:07:40 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id C2364824DD; Mon, 3 Sep 2018 19:07:40 +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 7917E824B2 for ; Mon, 3 Sep 2018 19:07:36 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=serge.lehuitouze@gmail.com; spf=Pass smtp.mailfrom=serge.lehuitouze@gmail.com; spf=None smtp.helo=postmaster@mail-ua1-f49.google.com IronPort-PHdr: =?us-ascii?q?9a23=3Ao2qvUBRm33/IU9g8foY5eZwoO9psv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6ybRyN2/xhgRfzUJnB7Loc0qyK6/+mATRIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf?= =?us-ascii?q?5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbD?= =?us-ascii?q?VwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4rx1QxH0li?= =?us-ascii?q?gIKz858HnWisNuiqJbvAmhrAF7z4LNfY2ZKOZycqbbcNwdWGRBQ91RVzRfDYyg?= =?us-ascii?q?c4sBAe0BPeNCoIn8oVsFsB+yCAaoCe/qzDJDm3340rAg0+k5Ew7G0gwuEdwNvn?= =?us-ascii?q?rJstv6KKgcXPupzKnR1zjPc+9a1Sv/5YXObxsvoeuMXbV1ccfJ1EcgCRnFjlqO?= =?us-ascii?q?pof4OT2ayPkGvWqG7+phSeKvjHMnqgBvrTOywcoskZfGhpgayl/a7yl5xJg6Jd?= =?us-ascii?q?2lSE56fd6kF4ZQtiCEOIZtTcMiRntnuCc+yrEcpZG7ey0KxY0hyhXCZfKHdI2I?= =?us-ascii?q?7QjiVOaXOTp4hXRleKi+hxmo60SgxPf8WtG00VlQripFld7MumoR2BzU78iKTO?= =?us-ascii?q?Z28ES52TuXyQzf9uVJLVo3mKfbMZIt3KA8moQJvUnMGiL7nlj9grWMeUU+4Oeo?= =?us-ascii?q?7vzqYrX4qZ+YMI95kgT+Pb4vmsy7GOg4LxIBU3WC9eSy27Du+Vf1QLpNjv0xna?= =?us-ascii?q?nZtI7VKd4Hqa6+Bg9Zyocj6xChADe6yNkUg2ULIVZfdB+Ej4XlIU/CLO7mAful?= =?us-ascii?q?jFmhlC9nx/XcMb3gBpXNIGLDkLDkfbtl8E5T1hAzzd9B6J5ODrEOPvLzWlLwtN?= =?us-ascii?q?zECR85Lg21zPj8BdVy04MRQ2OPAquDPKzOtl+I4/ojI/OQa48NpDb9N/8l6uby?= =?us-ascii?q?gnAjnF8debCl3Z8WaHCjAvRrOF6ZYHrpgtcZC2gGpAs+TOrwiF2DSzFffXiyX7?= =?us-ascii?q?hvrg08Xa6vE4bPcaWApoC7fW/vEpRIZ2wAD12KDW3lX4+JXesLYiuRJYlmiDNS?= =?us-ascii?q?Bpa7TIp07hy0uwKy77cvDvfV5ioFp5+rgMN4/eLe0xU/9SF1E8OAwWylQGR9n2?= =?us-ascii?q?dOTDgzivMs6Xdhw0uOhPAry8dTEsZesrYUC15rZ66Z9PRzDpXJYiyEe96ITFi8?= =?us-ascii?q?RdD/WGM+S9swx5kFZEMvQoz+3CCG5DKjBvour5LOHIY9q/uO0H34JsI7wHHDhv?= =?us-ascii?q?F40gsWB/BXPGjjvZZRsgjeA4mTzhecnqeuMLkVhWvDqDbFwm2Js0VVFgV3VPed?= =?us-ascii?q?UA=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CYBADlaY1bhjHeVdFbHQEBBQELAYNyA?= =?us-ascii?q?UB/KINyg3eQSYINAoJXhnaHIIc4CyOESQKDRxkHAQQzFQECAQECAQEBAQETAQE?= =?us-ascii?q?BCAsLCCkjDII1JIJfAQUjHQEbEgsBAwwGBQsNAgIJHQICIgERAQUBChIGExKDD?= =?us-ascii?q?wGBaAEDFQ+YDDyLC4ERBQEXgnYFg14KGSYDCleBbwIGEnmBIogrgheEJIMQgW6?= =?us-ascii?q?DAYJXAoZfCJRvBwKGNIEpiBwXgUBIhmuFZosniC8PIYE2gXdNI1AxgjsJghAag?= =?us-ascii?q?06BPokWPTCOEAEB?= X-IPAS-Result: =?us-ascii?q?A0CYBADlaY1bhjHeVdFbHQEBBQELAYNyAUB/KINyg3eQSYI?= =?us-ascii?q?NAoJXhnaHIIc4CyOESQKDRxkHAQQzFQECAQECAQEBAQETAQEBCAsLCCkjDII1J?= =?us-ascii?q?IJfAQUjHQEbEgsBAwwGBQsNAgIJHQICIgERAQUBChIGExKDDwGBaAEDFQ+YDDy?= =?us-ascii?q?LC4ERBQEXgnYFg14KGSYDCleBbwIGEnmBIogrgheEJIMQgW6DAYJXAoZfCJRvB?= =?us-ascii?q?wKGNIEpiBwXgUBIhmuFZosniC8PIYE2gXdNI1AxgjsJghAag06BPokWPTCOEAE?= =?us-ascii?q?B?= X-IronPort-AV: E=Sophos;i="5.53,325,1531778400"; d="scan'208";a="344728629" Received: from mail-ua1-f49.google.com ([209.85.222.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 03 Sep 2018 19:07:35 +0200 Received: by mail-ua1-f49.google.com with SMTP id m26-v6so900832uap.2 for ; Mon, 03 Sep 2018 10:07:35 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=bJjZFGJZ37F14pMyK/v3jI7qlk5KnTJbaHrY4GbvzkI=; b=F/aFK04pedu1EthVOG8wDNuXKNUyDe5UPVA5hrXRBTBV1XgvvVP/lGRPVs5IWOC/G3 f6Rqrw00cdOpDerHQLqoiZdkICMMClwh5ukwg0edvJqMA1gGzsn+RYABtHHNvRPprDnn 8aK6pYn+ozLg7+A+jOpjn8hyuaqRu1VlfX9M2OEkw2XygH/TPYfG+MxsFqDodtkO3Wbq ywK6ZjVDCzUo7qjzYjiXkZH+VngJLAD6fu8U/a+YKqpa3PSockCnWHJtuv5nmK4vpq0R J4/UUDTPbVEM2QiiHA6iFNdskL489sCjV1LxtM8XJjap+jqnKAGfVJKbuEhayHGmrWZZ zXwA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=bJjZFGJZ37F14pMyK/v3jI7qlk5KnTJbaHrY4GbvzkI=; b=X+gnuk1epFvaXPvhDm+N+wCnJM5oRjeI5SW23B1st57uHMfbAAJa/n5A61rmUwaNVn t4IJhdFXTsyhAeryx76Z4rE94kc6XbzIdXJUVDFguDVfBHSCiQYJ0iO5157MpuAcs5kU SO9JNpA+PtnEV0/uq0RO/yFKWKhWsYbPq4mqAj7e16YRIUmcUJNp24IBv0Groyg1fntT OaafILSkab+0/zY2NgaRjmmkvoJRUvKn9VbiOWcnNj8WaFLNKjWgf4IS/BcZNGMkVdZR R65lf//D7N9CcsEo1hQJEUabB0nB6mYR6BbyIL2hO0WmLLB9PFANyRAuCTXSNG9lfswa P/Mw== X-Gm-Message-State: APzg51C4K52nCM3Tqd5TfZwEeSjmHgrXreQfVen1Txd9bAN4tej7M1Wx vb3Qx1OmigivjnzGpcpO2pejG52QZzgGG87I2u42Lw== X-Google-Smtp-Source: ANB0Vdbg4v6jY/5oownRnWxFD6HSTsYLd5oiqSMeFU+aH5tl7nSjDXWEnPJD0Rdsm01/s3oWrNZ79SWegT29QSm15FU= X-Received: by 2002:ab0:5612:: with SMTP id y18-v6mr6199371uaa.3.1535994454636; Mon, 03 Sep 2018 10:07:34 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a9f:3767:0:0:0:0:0 with HTTP; Mon, 3 Sep 2018 10:06:54 -0700 (PDT) In-Reply-To: <30e39671-f6a3-cbd5-284e-ed23d4456adf@bentobako.org> References: <1C15EE94-097B-4758-815F-1F9D0BB5EF6C@ensta.fr> <30e39671-f6a3-cbd5-284e-ed23d4456adf@bentobako.org> From: Serge Le Huitouze Date: Mon, 3 Sep 2018 19:06:54 +0200 Message-ID: To: =?UTF-8?Q?David_MENTR=C3=89?= Cc: caml-list@inria.fr Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] FoCaLiZe 0.9.2 released Reply-To: Serge Le Huitouze X-Loop: caml-list@inria.fr X-Sequence: 17043 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: Hi all, I *don't* think it's inappropriate to answer to the list! --Serge On Mon, Sep 3, 2018 at 6:02 PM, David MENTR=C3=89 wrote: > Hello Fran=C3=A7ois Pessaux, > > > Le 03/09/2018 =C3=A0 10:38, Fran=C3=A7ois Pessaux a =C3=A9crit : >> >> 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 progr= ams > 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=C3=A9 > > > -- > 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 --=20 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=