This isn't so much directed at you, as other people that get inspired by this. I have been working on my own Rust like language with claude for a few months and there are a _lot_ of projects like that out there.

Mine has a formally proven borrow checker built on linear types, along with algebraic effects, with an LLVM compiler written in lean -- the type checker uses exactly the proven calculus.

If you are going to build a language with claude, I highly, highly recommend writing it in Lean or Coq and starting by formalizing a pre-existing paper or system that has the properties you want.

Claude gets confused and takes shortcuts constantly, and if you don't have a proven base, you are really going ot struggle. I had to throw away months of work as i got bogged down trying to resolve special cases and bugs that just evaporated when i switched to a proven calculus.