Haven't heard about since ages ago when it was extremely slow
I just checked out Flow and woah. First-class syntax sugar for React. Maybe cool. (If it doesn't break catastrophically in a sane build system like Vite)
Seems like they kind of did that? The thread seems like people already were waiting on this, so that's positive.
It seems backwards that they are freezing the Babel AST into the interoperability contract and only using the more efficient native representations in an isolated fashion -- shouldn't it be the other way around?
Trung0246•45m ago
jon-wood•37m ago
koito17•23m ago
Just cause it isn't used for webshit doesn't mean "approximately no one" has heard of it.
Lean is pretty much the most popular language mathematicians use today for computer-assisted proofs. More mature audiences may know about Rocq, Isabelle, etc., but Lean was already popular enough for a few people I know to have written their PhD theses on it about a decade ago.
I think GP is joking about a port to Lean because that would at least produce a formally verifiable output.
HeavyStorm•13m ago
I like Lean (and more generally dependent types) but ffs Lean has a very, very small userbase for a project like this. GGP would have to really justifyv the benefits for such a switch.
koito17•5m ago
In fact, I am not sure of any subset of Rust that is known to be formally verifiable. I know the Rust Foundation has funded *some* project in the past towards this goal, but that's orthogonal to the conversation.