Comment by reinitctxoffset

I hope to open source some of this soon but it's still married to quirky internal build tools and other jank. I'll make a note to come back to this comment when there's code up.

In terms of process I don't know that I really have any unique edge or anything, I'm still very intermediate as a lean4 programmer. I was a strong Haskeller before so I had a little bit of a map. The key thing about lean4 coming from e.g Haskell is that it has a much cleaner type tower, there's no type/kind/PolyKind jank, it's just Type 0, Type 1, as high as you care to go (which usually isn't very high), so a fair bit is unlearning some of that.

A mistake I made was to try to learn lean4 in emacs, which I'm working on making more reasonable, but today lean4 is a vscode only experience IMHO, this is partially because the default Mathlib4 style is really unapproachable without the tooling (not being a professional mathematician I'll stop short of calling the style bad, maybe it's intuitive to mathematicians, but it's very ill suited for programming in the large as a hacker would approach it). Proofs of theorems are this tactic match space with a lot of implicit projection up into a big possibility space at every step, and then the next explicit tactic is grabbing things from that space often very implicitly. It's my least favorite part of the semantics (or maybe one I feel is over-used, there are ways to make it more explicit, the canonical example is probably `simp_only` which grounds in specific lemmas).

The effectful part of the language should be a pretty short hop from anything else with do-notation, it reads very naturally and the conditional/looping/match stuff sorta looks like Rust if you squint a little. One place the AI assist really shines is to go rename all the variables something reasonable, a lot of otherwise great code looks like it hybridized with a bizarre Hungarian-notation splinter faction, the keywords are fine.

There's some stuff that probably makes a lot of sense in a meta mathematical view of things that makes zero sense from a TCB standpoint. To mathematicians there is a distinction between the map coloring proof and Wiles' FLT proof. This is real and it makes sense in mathematics. But in high-assurance software having an issue with `native_decide` as opposed to `bv_decide` is a weird religion: TCB certifying them is identically compromised by a compromised compiler.

So I think it's mostly just a very small community trying to write code as the primary activity and layering on formal methods as a correctness strategy as opposed to a much bigger community doing real maths where the programming language is more of an amenity than the main show.

I suppose my approach is to be willing to go a different way in a different use case.