4 ms·

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/ http

by buro9 15y ago

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/ 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 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 http://www.icfpconference.org/icfp2011/accepted.html

wladimir 15y ago
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.
- acangiano 15y ago
  > 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/fsharp/release.aspx http://research.microsoft.com/en-us/um/cambridge/projects/fs...
  - wladimir 15y ago
    Pretty cool. From that page they even provide instructions for Linux and Mac: http://functional-variations.net/crossplatform/ 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.
- yread 15y ago
  > 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)

by buro9 15y ago

wladimir 15y ago

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.

acangiano 15y ago
> 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/fsharp/release.aspx http://research.microsoft.com/en-us/um/cambridge/projects/fs...
- wladimir 15y ago
  Pretty cool. From that page they even provide instructions for Linux and Mac: http://functional-variations.net/crossplatform/ 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.
yread 15y ago
> 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)