search

fdilke / bewl

A DSL for the internal language of a topos
61 stars 3 forks source link

Lean 4 impl? #11

Open alok opened 11 months ago

alok commented 11 months ago

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 commented 8 months ago

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 commented 8 months ago

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.