Success in programming languages is not simply if-you-build-it-they-will-come. Bootstrapping a community that loves programming in it is the hard part. You'll either need a killer interop story with an already built ecosystem, or you'll need your own HTTP server, JSON parser, etc. etc. etc.
Best of luck! I'll watch this space.
That is good advice, I’m definitely planning on including some batteries soon, once I’m very happy with where the compiler is at.
On that note: allow me to "import" or "use" a C header without writing any FFI code.
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.
That is exactly my motivation. The purpose of adding effects to my language, for example, was at least partially so you can track changes to things like IO usage in PRs. I also plan on adding a simple proof DSL that surfaces some lean functionality directly into the surface, so you can prove invariants about code as in this language, or surface exactly what is being trusted when writing the equivalent of unsafe code.
The main thing I am trying to solve is the LLM code review problem, really.
1. I'm curious how this handles I/O? Proving stuff is often really useful for distributed systems where we would like to prove our system behaves correctly under any ordering of I/O operations.
2. How does this compare to just using Rust and some proof tool like Kani or Verus?
if you're all-in on ai, you want to prioritize familiarity for agents.
Also, what you're saying implies Python and Rust should stop evolving as languages, as changing the language would invalidate the vast quantity of work the AI has been trained on.
I disagree. It's not worth changing languages for new ones if you want to use AI, unless you can manage to create so much training data that it ends up baked into the models.
> Also, what you're saying implies Python and Rust should stop evolving as languages
Yes, much the way x86 assembly has stopped evolving for the user, outside of smallish additions like wider vector ops. Adding small, high value extensions extensions can be worth paying the token cost and increased failure rates if they add strong new capabilities.
If it's just ergonomic, it's a mistake, unless you want to target hand coders.
There are a shrinking number of reasons to geenfield projects with non-strict or unsafe languages now.