F★ for the masses (original) (raw)
- Apr 17, 2019
F* Summer Schools 2019
Here are a few summer schools that will have F* courses and that are coming up soon:
- The Oregon Programming Languages Summer School, Eugene, OR, USA (School: June 17-29,materials)
- Summer School on Verification Technology, Systems, and Applications, Luxembourg (School: 1-5 July,materials)
- Escuela de Ciencias Informáticas, Buenos Aires, Argentina (School: 22-26 July)
- Second International Summer School on Metaprogramming, Schloss Dagstuhl, Germany (30 June, School: 11-16 August)
The last two ones include a part about meta-programming in F* (tactics etc). - May 22, 2018
F* v0.9.6.0 released
On 18 May 2018 we released F* v0.9.6.0.
A large number of people contributed to this release: thanks to all!
Main new features
- Meta-F*: A metaprogramming and tactic framework, as described in this report. Code samples are in examples/tactics, examples/native_tactics and the
FStar.TacticsandFStar.Reflectionlibraries. Many people contributed a lot to this work, especially Guido Martinez. - Improved type inference with two-phase typechecking: We now build verification conditions for a program after a first phase of type inference. This improves inference of implicit arguments and reduces our trust in the type inference. Thanks to Aseem Rastogi!
- Caching typechecked modules: F* emits “.checked” files, an on-disk representation of a typechecked module that can be read back later. This significantly reduces the time to load a module’s dependencies.
...Read more - Jan 12, 2018
Lens-indexed lenses
In many functional programming languages, lenses are an increasingly popular, highly composable, way of structuring bidirectional data access, i.e., operations to both read and functionally update parts of a composite object. There are many introductory tutorials about lenses on the web: one that I found to be particularly gentle is by Gabriel Gonzalez. I’ll borrow some of his ideas to introduce lenses briefly here, although, of course, I’ll work in F* rather than Haskell.
Doing it in F* raises a couple of interesting challenges. First, programming with mutable references and destructive updates is common in F*: so, unlike some other lens libraries, ours must support mutation. Second, like everything else in F*, our lens library focuses on verification: we need a way to specify and prove properties about lenses in a way that does not compromise the inherent composability of lenses—composability being their primary appeal. My solution, the lens-indexed lens, is analogous to the monad-indexed monad, a structure at the core of the design of F* itself.
...Read more
- Nov 23, 2017
printf*
It must have been around 2002 when I first read a paper by Lennart Augustsson about a language calledCayenne. It was the first time I had come across dependent types. Lennart’s first example motivating the need for (and the power of) dependent types isprintf: a function used by legions of programmers that is, in an essential way, very dependently typed. Having worked since then on many programming languages with various forms of dependent types, now, 15 years later, a language that I contribute to has a proper, dependently typed printf. Well, a sprintf, but Cayenne’s example was also asprintf. This post is about explaining how sprintf works in F*.
...Read more
- Aug 24, 2017
F* v0.9.5.0 released
On 24 August 2017 we released F* v0.9.5.0. This is another big release with lots of changes and new features compared to v0.9.4.0.
Main new features
- Proofs by reification (see this paper)
- A revision of the libraries based on a new formal account of monotonic state (see this paper)
- Extraction of programs with user-defined effects
- Experimental support for tactics
- New IDE protocol and new IDE features: autocompletion, evaluation, real-time syntax checking, jump-to-definition, type-at-point, etc.
...Read more - Feb 9, 2017
Teaching F*
Having to teach F* provides strong motivation to dust off the cobwebs and tidy away long forgotten bread crumbs hidden deep down in remote directories to make the language easier to install and use. It is thus no coincidence that major releases have been aligned with some of us going back to school after a long summer of coding to step out there and present the newest features of the language to a crowd of rowdy students.
The latest two occasions:
- a Summer School on Computer Aided Analysis of Cryptographic Protocols in Bucharest, Romania, 13-14 September 2016 in which we had two days to teachVerifying Cryptographic Protocol Implementations with F*.
Who would have thought that F* can be used to introduce students of varying backgrounds to functional programming. This lead to theGentle introduction for F*.
This was the first time we used the universes version of F* for teaching and we thus had to updated the F* tutorial. We also played with docker builds to provide students with a preconfigured interactive mode, but most students stuck to the tutorial. - a MPRI course on Cryptographic protocols: formal and computational proofsin which we could spend more time teaching Program Verification with F*.
We for the first time taught low-Level stateful programming with hyperStack. Warning, this is so new that it’s not yet covered by the tutorial.
It is no coincidence that both courses had a decidedly cryptographic focus given that F* is the language of choice of the Everest project.
What features would you like to see included in future research schools? And what do you think are the biggest stumbling blocks when learning and teaching a hot-off-the-press research language like F*? - Feb 9, 2017
F* v0.9.4.0 released
The F* team is pleased to announce the release ofF* v0.9.4.0. This is the culmination of exactly one year of hard work from a very quickly expanding F* team. We’re not very good at keeping precise change lists, but here are the main highlights of this release:
- Predicative hierarchy of universes with universe polymorphism
- Uniform syntax between expressions and types allowing rich type-level computation
- Dijkstra Monads for Free
- Extraction to C via KreMLin
- New parser based on Menhir
- New pretty printer for surface syntax and
fstar --indent - Changed default effect to Tot
- Strict positivity check for inductives
- New synatax for inductive type projectors and discriminators
- Better semantics for module open and support for local opens
- Better dependency analysis
- Better error locations for Z3 failures
- Replaced Z3 timeouts with machine independent resource limits
- Cleaned up libraries and examples (a bit)
- Improvements to interactive mode
- Docker builds
- Fixed a ton of bugs (262 closed GitHub issues)
Enjoy the best F* release ever! - Sep 30, 2016
Introducing KreMlin
The work we do these days on F* is often in service of Project Everest. The goal of Everest is to verify and deploy a drop-in replacement for the HTTPS stack, the protocol using which you are probably reading this page, securely (hopefully). So far, we’ve been focusing most of our efforts in Everest on TLS, the protocol at the heart of HTTPS.
Right now, I’m stuck in the Eurostar back from our week-long meeting in Cambridge, UK, so it feels like a good time to write down some thoughts about KreMLin, a new compiler backend that we’re using in Everest, that several of us have been working on over the summer, at MSR and INRIA.
As a reminder, Everest sets out to verify and deploy secure cryptographic protocols, starting with TLS 1.3.Deploy is the salient part: in order to see people adopt our code, we not only need to write and prove our TLS library, but also to
- make sure it delivers a level of performance acceptable for browser vendors, and
- package it in a form that’s palatable for a hardcode Windows developer that started writing C before I was born.
A TLS library can, roughly speaking, be broken down into two parts: the protocol layer that performs the handshake (“libssl”) and the cryptographic layer that actually encrypts the data to be transmitted (“libcrypto”). The handshake connects to the server, says hi, agrees on which algorithms to use, and agrees on some cryptographic parameters. Once parameters have been setup, the cryptographic layer is responsible for encrypting the stream of data.
...Read more - Aug 26, 2016
Welcome to F*!
After many discussions, and in the spirit of the Gallium Blog (where I was a regular), the F* team is happy to announce the F*-blog! Expect a variety of posts, ranging from technical digressions about Dijkstra Monads to engineering discussions about parsing technology, and pretty much anything in between.
One of our stated goals is to make F* more accessible to beginners; this means making the setup easier, but also writing more documentation, so that people who are not in the vicinity of the F* team can write programs, too. We’ve started an effort on the wiki; the goal of this blog is to complement the wiki and make it easy for F* enthusiasts to keep up with the development; be notified about breaking changes on the master branch, and more generally make the development process more open.
I expect that this blog will also cover related projects, such asKreMLin, our F*-to-C translator, andmiTLS, our ongoing implementation of TLS 1.3 in F*. Stay tuned! ☭