I'm not using Jev yet (I'm on the waitlist), but I'm working on a programming language that I'd love to try to use Jev for spec/program/proof synthesis in (old exploratory repo

I'm not using Jev yet (I'm on the waitlist), but I'm working on a programming language that I'd love to try to use Jev for spec/program/proof synthesis in (old exploratory repo https://github.com/rokopt/geb ; new more "real" repo into which I'm distilling what I want to keep from the former at https://github.com/rokopt/geb-mathlib). One of its properties is a small and highly regular syntax, which I hypothesize/hope would be much easier to teach machines to speak than natural language, but I've been expecting that LLMs would still be monumentally inefficient because of all the baggage they carry to allow them to speak natural language, make videos, and so on. I'd thought some LLM or SLM tuned to highly regular programming languages would be vastly preferable (in the ethics of how its training data would be obtained, as well as its engineering qualities), but I hadn't found anything that looked both promising and active. Suddenly