Introducing F*: Secure Distributed Programming with Value-Dependent Types | Hacker News Reader

Introducing F*: Secure Distributed Programming with Value-Dependent Types

research.microsoft.com

51 pointsburo912 comments

Warning for those downloading the PDF on that page, it's 1.6MB.

There is also a compiler project here: http://research.microsoft.com/en-us/projects/fstar/

And you can try out F* (by validating code) on the web here: http://rise4fun.com/FStar

And for anyone who has noticed my submissions in the last couple of days, I'm basically reading my way through the SIGPLAN papers for ICFP 2011 and picking out interesting things that others might like too: http://www.icfpconference.org/icfp2011/accepted.html

It seems that Microsoft is doing extremely interesting fundamental CS research (especially into automated verification/program correctness/security) these days. I'm enthusiastic about it, though I somehow fear the end result will at most be some expensive proprietary extension to Visual Studio only targeting .NET instead of an open implementation benefiting everyone.

> I somehow fear the end result will at most be some expensive proprietary extension

That hasn't been the case with their research, so far. See F#'s download page for an example: http://research.microsoft.com/en-us/um/cambridge/projects/fs...

Pretty cool. From that page they even provide instructions for Linux and Mac: http://functional-variations.net/crossplatform/ . So the F# "source drop" is licensed under the Apache2 license?

I guess I should give them the benefit of the doubt, it's just a bit difficult for me given their track record.

> interesting fundamental CS research (especially into automated verification/program correctness/security) these days

As far as I know they are doing it for looong time (look at Spec# for example). They needed it for the driver WHQL verification (they actually verify that the drivers fulfill some temporal logic predicates)

Hmmm, they didn't verify the correctness of the translator or CLR?

Verification does not need to be an all of nothing approach. Having one part of a system verified means that you are sure certain bugs can't appear on that code. So, there are less bugs in total, and when facing such a bug you know where you don't need to look. Otherwise you never end, you have to verify your code, the compiler, the operating system, the processor, quantum physics, the creator of the universe...

That's not quite true. You can't make any assertions about the behaviour of the system if only one part of it is verified.

The way to verify the entire system is not to verify that quantum physics works; that doesn't help. Instead you have to assume that the logic gates you are using are deterministic which is impossible to prove. Then you work up from there.

Despite this, I do agree that having part of the system verified is better than having none of it verified.

If you verify the correctness of the CLR, by the same reasoning don't you have to verify the correctness of Windows as well?

If you verify the correctness of Windows, don't you have to verify the correctness of all the parts in the hardware stack?

Yes, I hadn't thought of that. The point is that proving part of a process correct without proving correct the entire stack, is no guarantee that it does anything like what it's supposed to.

But, if you don't even try to prove part of a process correct, it's almost certainly wrong. See the excellent work that John Regehr's group is doing related to compiler and optimization verification/testing (http://www.cs.utah.edu/~regehr/research/ ), much of which has been talked about here.

There are other folks who have successfully done formal verification of operating systems, device drivers, hardware design, etc. It's a big, hard problem, but we'll get to the "whole stack" eventually.

Reply on news.ycombinator.com