Hi Bas, We've made several attempts at formalizing various fragments of F*, none of which establish consistency of the full language (unsurprisingly).
Our most recent attempt is in a paper at POPL 2017: https://www.fstar-lang.org/papers/dm4free/ There, we present a calculus called Explicitly Monadic F* (EMF*) which includes the pure fragment of F*, with dependent types, refinement types and user-defined monadic effects. EMF* excludes many F* features too (especially the following, which are particularly relevant for consistency): 1. inductive types and pattern matching 2. F*'s let-rec primitive (and its semantic termination check) 3. a typing rule that supports type conversion based on provable equality 4. divergence encapsulated in another effect 5. the encoding of F*'s logic to first-order logic provided by an SMT solver For this limited EMF* calculus, we have a syntactic metatheory proving total correctness of the WP-based program logic we derive for effectful terms. Extending EMF* at least with features 1, 2, and 3 above and studying its consistency would be very interesting ... well, at least to the few of us who work on F*. That said, the main theorem of this POPL '17 paper is to establish the correctness of a CPS-based transformation to derive WP calculi from definitions of a monad. This is done by a logical relations proof on EMF*. Other papers have attempted to study some of these other consistency-related features of F* in slightly different settings: -- https://www.fstar-lang.org/papers/mumon/ this one includes a proof of normalization of a small calculus ("pico F*") with recursion, refinement types and our termination check -- This short paper https://hatt2016.inria.fr/files/2016/06/HaTT_2016_paper_1-5.pdf formalizes a core of F*'s encoding to first-order logic Aside from all this, there's the question of the correctness of F*'s implementation: of course, F* is under active development and we find, fix and (sadly) introduce correctness bugs from time to time. We hope someday to revisit our work on "self-certification" (https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/popl2012-paper211.pdf) and apply a technique like it to the current implementation of F*. Hope that helps, Nik > -----Original Message----- > From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> On Behalf Of Bas > Spitters via fstar-club > Sent: Friday, June 29, 2018 3:30 AM > To: fstar-club@lists.gforge.inria.fr > Subject: [fstar-club] Consistency of F-star ? > > What are the current conjectures, thoughts about the consistency/semantics > of F*? > > Could you point me to a paper I should read? > > Thanks, > > Bas > _______________________________________________ > fstar-club mailing list > fstar-club@lists.gforge.inria.fr > https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gf > orge.inria.fr%2Fmailman%2Flistinfo%2Ffstar- > club&data=02%7C01%7Cnswamy%40microsoft.com%7C428fa932a4c04 > d1ce84708d5ddabaec4%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0% > 7C636658651809180794&sdata=EEKoy3UGxk%2BOKuLGPDTQb%2F0AZ > %2FhMKcc7PzI09bvk5Og%3D&reserved=0 _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
