Have you seen https://github.com/FStarLang/fstar-vscode-assistant? Copilot & F* works pretty nicely.

We've also had a pretty nice emacs mode for a while: https://github.com/FStarLang/fstar-mode.el

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

Some of it is deployed in production systems:

* Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-hard...

* Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star

So _would_ it possibly be useful for business apps? Or is that still a long way off?

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.

After C#, I learned F#, I loved language structure, but I was not able to run it on production effectively.

A language isn't enough, a language recognized from its support in ide/production and community

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#.

Ionide, The F# language server, is excellent.

I use F# in .NET Interactive Jupyter notebooks daily at work and it works quite well.

The community around the language is very helpful and the Discord is great for all sorts of issues ranging from beginner to advanced.

I love the Fable compiler which targets JS, TS, Python and Rust and makes for a wonderful way to share a domain design across multiple code bases.

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.

Where do you even find orgs that let you program in those fun langs?

University jobs?

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.

2017 was right as the very first releases of .NET Core 1, 1.1 and 2.0 were happening.

It’s most likely your experience today would be a polar opposite to this.

There are some trading companies as well, I guess because it's ocaml adjacent.

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

Maybe I am remembering this: https://en.wikipedia.org/wiki/ATS_(programming_language)

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.