From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 0D34F7F730 for ; Thu, 16 Mar 2017 15:07:12 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tom.j.ridge@googlemail.com; spf=Pass smtp.mailfrom=tom.j.ridge@googlemail.com; spf=None smtp.helo=postmaster@mail-ot0-f180.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of tom.j.ridge@googlemail.com) identity=pra; client-ip=74.125.82.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tom.j.ridge@googlemail.com"; x-sender="tom.j.ridge@googlemail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of tom.j.ridge@googlemail.com designates 74.125.82.180 as permitted sender) identity=mailfrom; client-ip=74.125.82.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tom.j.ridge@googlemail.com"; x-sender="tom.j.ridge@googlemail.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-ot0-f180.google.com) identity=helo; client-ip=74.125.82.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tom.j.ridge@googlemail.com"; x-sender="postmaster@mail-ot0-f180.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AGvMiFR83btaoev9uRHKM819IXTAuvvDOBiVQ1KB3?= =?us-ascii?q?1eIcTK2v8tzYMVDF4r011RmSDNidtaoP0LeempujcFRI2YyGvnEGfc4EfD4+ou?= =?us-ascii?q?JSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgpp?= =?us-ascii?q?POT1HZPZg9iq2+yo9ZDeZwVFiCC8bL9uIxm7owXcvdQKjIV/Lao81gHHqWZSde?= =?us-ascii?q?RMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZ?= =?us-ascii?q?TQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6KhlVQLoiD?= =?us-ascii?q?wfNzEn7G7XlsJ+jKVeoB27phx/xZPfbIWaOfd6e6/Qe84RS2hcUcZLTyFOAI28?= =?us-ascii?q?YYsBAeQCIOhWsZXyqkAUoheiHwShHv/jxiNKi3LwwKY00/4hEQbD3AE4AdwOt3?= =?us-ascii?q?HUp8jpOqcTTO+1w7fHxijEYvNK3jf97ZLEchI7rfGWXLJ/bMXRxlcoGwPBj1WQ?= =?us-ascii?q?spDlMiia1uQKtGib4O5gWvyqi2E9qgFxpiKjydsrionMn48YzE3P+yt+wIYwP9?= =?us-ascii?q?K4SUh7bMalEJtWrSGaNpF5TtksQ2FyoCo6xbwGuYK7fCgX05sr3QLQa/uCc4SQ?= =?us-ascii?q?4hPsTuaRITB/hH5/ZL2/gBOy/E69weP/Tsm5yFRHoyVfntXRqHwA1wbf58uZRv?= =?us-ascii?q?dn40us2iqD2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmErsja+Wclwo+u+0?= =?us-ascii?q?6+j7e7nmqIKQOoxohg3kPaQuncu/Aes8MgcQRWSU5eO81Lj78U34RrVFkOE2n7?= =?us-ascii?q?HbvZ3VP8gXu7C1Dg9P3osg9RqzFSqq3dcEkXUfKVJKYhOHj4znO1HUJ/D4CO+y?= =?us-ascii?q?g0irkDdu3fzGPKftAo/MLnfen7fuY61w60FbyAo0wtBf44xbCrQbL/LyXk/9rs?= =?us-ascii?q?DXDhg8MwCs2eboFM191p8CWWKIGqKWLLndsVqM5u42J+mMZZQVuCrmJvg+5//u?= =?us-ascii?q?iGc5lkUHcamo25sXcnG4Ee58L0WXe3q/yusGRGwDuw57SO3xlBXWWjdWYzO2Xr?= =?us-ascii?q?kgzjA9EoOvS4nZENODmruEiRu8G9VsZ2xJBxjYDXDtMYfCQfYAZy/RJs56jhQL?= =?us-ascii?q?Ur+uT4Ik3BCq8gT9zuw0faLv5iQEuMe7h5BO7OrJmERupDE=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CPAABxm8pYhrRSfUpeGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBhAeBCgeDWptngjqTBYI4hXiCfwdAFwEBAQEBAQEBAQE?= =?us-ascii?q?BEgEBAQgLCwgoL4IzCoJYAQECAgEjHQEtDAMMAQUFCw0NHQICIhIBBQEKEgYTE?= =?us-ascii?q?olVAQMNCA6kHD+MA4ImgwkFg2AKGScDCoMaHgIGEosrglGBb0GCWYJfBYdADJR?= =?us-ascii?q?5hneLR4JPjlqSBRQfgRUPEQGBOhMREAUfVheCZ4EVCyqCD0A1AYcLgjwBAQE?= X-IPAS-Result: =?us-ascii?q?A0CPAABxm8pYhrRSfUpeGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBhAeBCgeDWptngjqTBYI4hXiCfwdAFwEBAQEBAQEBAQEBEgEBAQgLCwgoL?= =?us-ascii?q?4IzCoJYAQECAgEjHQEtDAMMAQUFCw0NHQICIhIBBQEKEgYTEolVAQMNCA6kHD+?= =?us-ascii?q?MA4ImgwkFg2AKGScDCoMaHgIGEosrglGBb0GCWYJfBYdADJR5hneLR4JPjlqSB?= =?us-ascii?q?RQfgRUPEQGBOhMREAUfVheCZ4EVCyqCD0A1AYcLgjwBAQE?= X-IronPort-AV: E=Sophos;i="5.36,172,1486422000"; d="scan'208,217";a="216985855" Received: from mail-ot0-f180.google.com ([74.125.82.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 16 Mar 2017 15:07:10 +0100 Received: by mail-ot0-f180.google.com with SMTP id x37so56432165ota.2 for ; Thu, 16 Mar 2017 07:07:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20161025; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to; bh=Ert2HeQH/9fnHgZCiPxQe9jJYQEjh/2gzpkl+wg3BQg=; b=Yed3hAVvYdAKatvjA/HkSzBBJu0bjybZnpvivsgjUjlOxrGiowLF5s5XjqdnapcMx7 3HQms6J3OY5iika8t/YCxOxxd/2Fzx3dnCu77s8dJJJDJiu4AktoC4M2F9IMJCiSawj2 H3fhQnnGtjHhEz5CR0H2TBHYmBxNoKnOZCev0TfgsfIhoCRp1HAtLuSvZcqJo/pc6fb+ kRuTyA6x8aQSkCKc/CGBdmJGon+EfCd+Gdpja7qAyFMXfHcNsgLFM8WvZeoVEJlbCkUC xdpQ8UotQofuFSpIJtCwCw50C/6PYAaTFhZMCjhg7Rpssjoc5HVdNKJ0Wetpvh8Dt14A dHJg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:sender:in-reply-to:references:from :date:message-id:subject:to; bh=Ert2HeQH/9fnHgZCiPxQe9jJYQEjh/2gzpkl+wg3BQg=; b=s4FgpQvOoBAIe7+1O5WkdHb9ualwtyF+8Ahsf2hFjqogi17bod2oqtACPr19gd3IXT uE+U7VkcvuJ5u5RJBqEMeLMslKcSvEqusBQdEid8QU57Qxr9GT5Q1Xqd1y9XTI4TgePu 69vm19vJvc2MWLyFeI5K0gwhMEsqntttS5J9FtTxT8hJ9gVeh3eUlEAS/xQUFH83KZk2 GOrJJD+4Syyvk9JwxQIppIf58DI12a+wmp47S0d/ZmcjctxfyZoNqZ6BHWgMnEMGXDo6 HBpUTAToWldZ/2DaapGw1VtWXyKkZ/VAcI1CG/OtvBVyJFQqrc6iHni6MujM34eqAwLm 08Uw== X-Gm-Message-State: AFeK/H03zOk4G4CiiGwNhSMsCMsufCEfQzdXJboJV6jNjMJdYMRY0g/odPSj85XYKSh45TkXgr4fhjoNwbmbqQ== X-Received: by 10.202.108.206 with SMTP id h197mr2129660oic.61.1489673229132; Thu, 16 Mar 2017 07:07:09 -0700 (PDT) MIME-Version: 1.0 Sender: tom.j.ridge@googlemail.com Received: by 10.74.144.129 with HTTP; Thu, 16 Mar 2017 07:06:48 -0700 (PDT) In-Reply-To: References: <20170316135331.GA21804@topoi.pooq.com> From: Tom Ridge Date: Thu, 16 Mar 2017 14:06:48 +0000 X-Google-Sender-Auth: kZAI55Sr8HQntRC-0dspNuIHqtg Message-ID: To: caml-list Content-Type: multipart/alternative; boundary=001a1142e094a76b38054ad993ad Subject: Re: [Caml-list] Preview: B-tree library --001a1142e094a76b38054ad993ad Content-Type: text/plain; charset=UTF-8 On 16 March 2017 at 14:05, Tom Ridge wrote: > > > On 16 March 2017 at 13:53, Hendrik Boom wrote: > >> On Thu, Mar 16, 2017 at 01:35:26PM +0000, Tom Ridge wrote: >> > Dear All, >> > >> > This may be of interest for people thinking about on-disk storage etc. >> > >> > https://github.com/tomjridge/tjr_btree/ >> > >> > It is not really in state to release, hence the "preview". >> > >> > It is the core library in the upcoming "ImpFS" filesystem which (with >> > SibylFS) comes from the "Future filesystems" project. >> >> The intereseting point about this syste is in the README: >> >> tjr_btree is a B-tree library. The core is written in Isabelle/HOL and >> exported to >> OCaml >> >> Does this mean something like that the code has been generated from a >> ormal proof >> of its correctness? >> > > Not at this point. But yes, previous versions have had (often partial) > formal proofs developed. So I would say that the code is likely to be > pretty good from a correctness point of view. Obviously the full formal > proof for the core would be desirable. But other projects can probably > start using the code now, hence why I released it relatively early. > > >> >> -- hendrik >> >> > >> > Thanks >> > >> > -- >> > 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 >> >> -- >> 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 >> > > --001a1142e094a76b38054ad993ad Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable


On 16 March 2017 at 14:05, Tom Ridge <tom.j.ridge@googlemail.= com> wrote:


On 16= March 2017 at 13:53, Hendrik Boom <hendrik@topoi.pooq.com> wrote:
On Thu, Mar 16, 2017 at= 01:35:26PM +0000, Tom Ridge wrote:
> Dear All,
>
> This may be of interest for people thinking about on-disk storage etc.=
>
> https://github.com/tomjridge/tjr_btree/
>
> It is not really in state to release, hence the "preview". >
> It is the core library in the upcoming "ImpFS" filesystem wh= ich (with
> SibylFS) comes from the "Future filesystems" project.

The intereseting point about this syste is in the README:

tjr_btree is a B-tree library. The core is written in Isabelle/HOL and expo= rted to
OCaml

Does this mean something like that the code has been generated from a ormal= proof
of its correctness?

Not at this = point. But yes, previous versions have had (often partial) formal proofs de= veloped. So I would say that the code is likely to be pretty good from a co= rrectness point of view. Obviously the full formal proof for the core would= be desirable. But other projects can probably start using the code now, he= nce why I released it relatively early.
=C2=A0

-- hendrik

>
> Thanks
>
> --
> Caml-list mailing list.=C2=A0 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

--
Caml-list mailing list.=C2=A0 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


--001a1142e094a76b38054ad993ad--