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.
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.
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.
I remember reading (~10 years ago) that F* was created as part of a "Project Everest" a long time back, with the goal of creating a provable TLS implementation. I never saw that anything came out of that though. If it's that hard to create something as well-defined as a TLS implementation, it seems futile to think this could ever be used for hand-wavy things we encounter in day-to-day work, no? Or are there real-world use cases where this could really be applied?
F* existed before Project Everest, but Everest did power a lot of its development.
We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/
The Everest project did publish a proved TLS implementation: https://mitls.org.
And at least the EverCrypt* cryptographic primitives has been used outside of academia.
I have not tried the VSCode stuff, but I did try the Emacs thing. Looking at the repo you linked, it looks like the first commit was last year and I left Jet in 2018.
The Emacs mode was fine, I didn't think it was bad, but it was still a tough sell to my team; none of them wanted to install Emacs, they wanted a Visual Studio or JetBrains experience. I'm aware that's an uphill battle, and maybe it would be a different story if the VSCode extension existed in 2018.
I didn't find F# so hard to run in production, particularly after JetBrains released Rider, but even before that I didn't think it was so bad.
At Jet we managed to get to pretty decent scale with F#, and for the most part got pretty ok performance. Often I would use the C# versions of libraries simply because they were updated more frequently. Everyone says that the C# interop is clunky and I think that's just not true, I found it relatively easy to work with C# libraries and utilize the .NET Framework. I used ConcurrentDictionary and SemaphoreSlim pretty heavily, for example. For the stuff was a little cludgy, I found it pretty straightforward to simply make wrapper functions that did what I needed.
I even found the object-oriented support in F# to be pleasant, though I didn't use it a lot. The syntax was really terse but easy to read, so in the rare cases where I had to extend a class or something, it wasn't hard. If I needed to implement an interface, it was also pretty easy to write an anonymous interface and plop that into a wrapper function.
One thing that I didn't like about F# was the kind of unpredictable performance with the async monad. It was hard to measure, and it didn't seem to work completely deterministically due to some kind of laziness that I never completely understood. The task monad released a bit later seemed to fix that, but that was integrated a bit later than my time at Jet.
Still, I found it a pretty decent language, to a point where if I started a company I would genuinely consider utilizing F#.
I haven't really used the Ionide plugin for VSCode, but I did make pretty liberal use of the Emacs plugin (well, Spacemacs), and it was pretty solid. I used it almost exclusively for about a year; I don't know if the Emacs plugin uses Ionide behind the scenes, but I thought it was pretty decent overall.
Still, once Rider got a few updates and was stable, it was kind of hard to go back. I'm a pretty dedicated Vim dude normally, but for a lot of "enterprisey" things like .NET and Java the ability to do smart refactoring of lots of files and integrated debuggers really do become a pretty substantial value-add for me.
I was working for Jet.com, it was one of the very few places that did F#. The reason I was hired was because I had Haskell experience from working at NYU as an engineer before.
I used F# at realtyshares in 2017. Didn't think it was particularly great for anything except Payment processing. The F# tools were only good with VS IDE on Windows at the time. I would probably use it again though, the REPL is much better than anything C# has to offer.
The Rider release was a shitshow, lots of bugs that went unfixed. Productivity went way down when I had to switch to a mac laptop (keep in mind this is 2017 on a Microsoft language). Had similar experiences with Rubymine in 2022 (poor YARD support, lots of bugs in type inference even with simple things, bug tickets left open for years, thank god for Sorbet-lsp). The tooling is probably better these days but I don't trust Jetbrains for anything, they are a rent-seeking company.
Maybe try looking for Clojure jobs? They aren't super common but are a lot more so than any other lisps or functional languages that I'm aware of (except maybe Scala).
Lately I've been dabbling with lean. pretty tight vs code integration. I don't know why I keep getting pulled toward dependent types, like a damn moth to a flame. I get a little scorched, then, oh I should try ...
But yeah, compiler checked properties are something kinda magical. Even more when you can specify the property to check.
Lean is lovely, but those of us using it for general purpose programming are a lonely bunch; virtually all discussion on Zulip is about mathlib and tactics (which is understandable).
I have heard of Lean, but I just took a look for the first time. Certainly, much more Idris/Haskelly than the OCamlish F*.
Are there libraries available for general programming in Lean? Can you compile to another lower-level language like C?
I would be interested in writing some embedded code that could formally be verified. Right now, I have put some time in to SPARK2014, the subset of Ada.
Lean in fact compiles to C so the C FFI is trivial to use. However, the only general programming facilities Lean has seem to be those required to bootstrap the language. I find it equal amounts funny and sad that you still cannot get the Unix epoch in Lean; you need to call the C functions through the FFI.
For verifying code Lean is not great right now (see a sibling comment in this post). For embedded code in particular, I remember there was a low-level formalizer, but I cannot remember what it was. This post here has many discussions and links: https://news.ycombinator.com/item?id=31775216
But I was under the impression there was an almost assembly-level functional programming language with formal verification capabilities; I cannot recall it.
Thanks, I had looked at ATS many years ago, but I had forgotten about it. I'm going to look at both Lean and ATS, but I guess I'll stick with SPARK2014 for work now.
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.
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.