Thanks, good advice!
Aside: To some degree, the claudisms are the point since the PL is written by Claude and intended to be consumed by claude
Re:Lean Now Ships with Verified Kernels
by thejokeisonme on Tuesday October 20, 2026 @04:53AM
(#50163154)
Re aside: Ok, but consider that maybe it is rude to ask people to read something you didn't write without warning. I'd add a disclaimer whenever I post about it, and on the very top of the readme. Better: have a readme for humans that you wrote, and leave the current document as a readme for machines.
You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.
Not saying your niche doesn't have value, but you can get interesting ideas from there.