Man, back when I did F# for a living, I really really wanted to use this for production, but I could never quite get sign-off. I was a big fan of Idris at the time, and F* seemed like it could more or less satisfy that itch while still being compatible with F#. One thing is that there didn't really appear to be any kind of IDE support, and while I'm alright just hacking up everything in Vim, I think the rest of my team was not.<p>I never really got to use it, and all I've ever done with it is a few of the toy examples on their website, but I haven't completely given up on it either. I think it's a much more approachable system than Coq or Agda, but still gives you sexy dependent types.<p>My PhD stuff is in Isabelle, and I do really like Isabelle, but I find that dependent types translate a bit more directly to "real code" than Isabelle's higher-order logic, so I would really like to utilize it for something, particularly with its .NET integration.