Lean 4 impl?

[alok]

You’d mentioned rewriting it in idris and scala 3. Another candidate is lean 4, which has a lot of the groundwork but no topoi yet. https://news.ycombinator.com/item?id=37430899

Stuff like gpt-engineer can help there with rewrites btw.

[fdilke]

That would be a really interesting project, but ATM Bewl does calcuilations inside the actual topos (with pluggable implementations for locally finite topoi), not proofs using topos logic.

[alok]

I'm more interested in its computational than proof ability. Nice thing about lean is it combines a real programming language with a theorem prover. Most languages pick just one.