[fstar-club] Slack forum open to all

Dear all, We recently opened up a slack forum https://everestexpedition.slack.com/ that was previously used mainly by members of Project Everest. Many F* experts, including the F* developers, hang out there regularly---it's a good place to ask questions about F* as well as many projects that

Re: [fstar-club] fibonacci_greater_than_arg solution

Hi Michael, Thanks for your note. The explanation for that proof isn't quite right---it supposes that Z3 automatically proves that fibonacci(n) >= 1, which it cannot do, since that requires an induction. Instead, the proof goes something like what's shown below. Thanks to Aseem for coming up

Re: [fstar-club] Execute F* using ocaml/opam package

Hello Marius, Some responses to your questions are below. Sent from Outlook From: fstar-club on behalf of Marius Melzer via fstar-club Sent: Tuesday, September 1, 2020 3:00 PM To: fstar-club@lists.gforge.inria.fr Subject:

Re: [fstar-club] FStar school

And also one covering Meta-F* (tactics etc.) in Buenos Aires in July https://eci2019.dc.uba.ar/cursos.html -Nik > -Original Message- > From: fstar-club On Behalf Of > Catalin > Hritcu via fstar-club > Sent: Tuesday, April 2, 2019 1:02 PM > To: Marc Gourjon > Cc: FStar Club > Subject:

Re: [fstar-club] Noob questions

Dear Christian, Thanks for your interest in F*! I respond to some of your questions quite broadly below. I’ll let others respond further with more specifics. -Nik From: fstar-club On Behalf Of Christian Nyumbayire via fstar-club Sent: Wednesday, January 9, 2019 6:42 PM To:

Re: [fstar-club] Consistency of F-star ?

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