I'm working on something similar. Dependently typed, theorem proving, regular syntax, long form english words instead of symbols or abbreviations. It's not very well baked yet but claude/codex are already doing really well generating it. I expect that once the repo has been around long enough to be included in training data it'll improve. Probably next year or the year after.

I'm looking for a language optimized for human use given the fundamental architectural changes in computing in the last 50 years. That way we could skip both the boilerplate and the LLMs generating boilerplate.