F*: A Verifying ML Compiler for Distributed Programming | Hacker News Reader

F*: A Verifying ML Compiler for Distributed Programming

research.microsoft.com

45 pointsprimodemus9 comments

Microsoft Research does some interesting stuff, though I have to take issue with their choice of naming. One wonders if they're trying to poke at search engines.

The "#" in C# made it painful, in the beginning, to craft a good query. Now they're using a symbol commonly interpreted as a wildcard.

I'm not insinuating any evil intentions with the name (that's a little ridiculous since it's an experimental language to begin with), but it's a little odd that they'd choose something that will likely be search engine unfriendly... again.

Stick to criticizing the paper.

Then you can write a blog rant about how painful it is to refer to "the second-order (polymorphic) lambda-calculus with bounded quantification" as F-sub or F<sub><=</sub>

Does anyone have experience running the languages coming out of Microsoft Research on Mono? I have no experience with C# or Mono, but I am interested in having a go with F* and would appreciate any guidance someone more familiar with the tech stack might have.

Microsoft has some minimal degree of support for F# on Mono. It is not the core focus for the F# team, but they do get to spend some time on it currently. Give it a shot.

Yep, F# works well, and Miguel de Icaza et al. are playing with it.

To get F# running with Mono, you'll want (at least on Linux) Mono 2.8+, and either MonoDevelop 2.4 (for which Thomas Petricek's language plugin works) or your own editor. I've mostly been using the stand-alone REPL and tweaking some Vim syntax highlighting.

I have to say, F# and now F* are about the only languages that could tempt me to give Mono a try.

I do know Banshee is written in C# and runs pretty well on Mono, but that was an application specifically intended for that application.

You can definitely run F# on Mono. Since F* seems to be an extension of F#, it might work on Mono too, but I don't know that for sure.

A lot of what comes out of MS Research ends up in their mainstream Visual Studio supported languages, so I would not be surprised to see at least some of F* get rolled into F# vNext, and maybe eventually C# too.

These MS language developers play for keeps don't they? First Spec#, now F*...

But seriously, this is good stuff. I wonder how long it's going to take for this kind of proof-driven code to reach mainstream programmers? Decades I imagine.

Reply on news.ycombinator.com