Home » forums » LtU Forum

F*: A Verifying ML Compiler for Distributed Programming

Interesting to many of you, I'd imagine -> F*

"F* is a new dependently typed language for secure distributed programming. It's designed to be enable the construction and communication of proofs of program properties and of properties of a program's environment in a verifiably secure way. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based."

C

By Charles Torre at 2011-07-23 19:25 | LtU Forum | previous forum topic | next forum topic | other blogs | 17036 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

F-star is F-aster in some languages :)

That's a pretty sweet name for a language.

Pierre-Yves Strub, Cedric Fournet, and Nikhil Swamy, Mechanized soundness proofs for F*, 1 April 2011

Seriously? They released their soundness proofs on April Fool's Day?

(From: Secure Distributed Programming with Value-dependent Types): To date, we have programmed and verified more than 17,000 lines of F* including (1) new schemes for multi-party sessions; (2) a new zero-knowledge privacy-preserving payment protocol; (3) a provenance aware curated database; (4) a suite of 17 web-browser extensions verified for authorization properties; and (5) a cloud-hosted multi-tier web application with a verified reference monitor.

Thanks for sharing this with us, Charles.

By dmbarbour at Sat, 2011-07-23 20:53 | login or register to post comments

You can play around with the

You can play around with the language here: http://rise4fun.com/FStar

Rise4Fun is a great playground. Need to spend more time there...

You're welcome, David! I know the researchers behind this would love some feedback. The bits are available here.

C

By Charles Torre at Sat, 2011-07-23 21:06 | login or register to post comments

A melting pot of type system hotness

I read the beginning of the IFCP11 paper, and it sure looks interesting. The (vastly underinformed) feeling I have is that F* is a mix of different type system features that had been studied in isolation and were known to work on specific domains (eg. linear or affine types for effectful resource handling), bringing them all together and still trying to be vaguely tractable for users.

More specifically -- but I'm just paraphrasing the paper introduction:
- F* separates "pure and total terms", for specification, and a Turing-complete sublanguage, for computation, by using kind distinctions
- F* uses affine types ("use at most once"), again classified by kinding, for modeling resource and effects
- F* proof language have both erased proofs (like Coq's Prop) and non-erased proofs, to be able to dynamically send proof witnesses in distributed contexts; again, this distinction is seemingly done by kinding

Their proof and specification language(s) is-are expressive enough to describe various domain-specific logics for authorization, authentification, etc. That allows them to work on applications that combine various types of formalization that were previously handled by specialized ad-hoc proof systems. They also seem to make generous use of SMT solver technology, when appropriate.

Their compilation process is strongly typed, and they produce as output "RDICL, a dependently typed dialect of .NET bytecode". I hadn't followed the previous work, and this sounds definitely impressive. It seems that the selective use of erasure helped make this tractable, by reducing the size of the resulting bytecode.

Finally, they have formalized a large part of the theory. This is impressive for a type system that is so large, that must really have been a lot of work. But this is also a situation where mechanized verification really pays off: I'm not sure I would trust a hand-made and eye-verified proof on a so large and complex system.

This paper briefly mentions "value-dependent types" as a restriction of full dependent types that simplifies the metatheory without empeding expressivity too much. In a nutshell, only values, not applications or any non-value expression, are allowed to appear in types. I would be interested in reading more about that, but I can't find the technical report associated to this paper; it has a webpage, but no download link that I can find.

Well, then I guess I need to read the full paper carefully. Definitely impressive.

By gasche at Sat, 2011-07-23 22:05 | login or register to post comments

Refinement Types

Here's a link to a paper with more detailed information related to refinement types.

By Charles Torre at Sun, 2011-07-24 00:19 | login or register to post comments

value-dependent types

This paper briefly mentions "value-dependent types" as a restriction of full dependent types that simplifies the metatheory without empeding expressivity too much. In a nutshell, only values, not applications or any non-value expression, are allowed to appear in types. I would be interested in reading more about that, but I can't find the technical report associated to this paper

This sounds similar to the restricted dependent types that ATS provides. The paper that Charles refers to on refinement types in another reply references one of Hongwei Xi's papers on dependent types so you might find the ATS papers interesting reading on the subject.

By doublec at Tue, 2011-07-26 04:43 | login or register to post comments

I can't wait for F***

The 3rd release will be the best.

By justncase80 at Thu, 2011-07-28 22:00 | login or register to post comments