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 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