Hacker News
points by empath75 3 days ago | 0 comments
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.

[–] amccollum 3 days ago
Is your language available anywhere? I'd be curious to check it out. I strongly believe that there will eventually be a new language created with agents in mind as the primary consumers, and making the foundations provable / safe are key cornerstones in my mind. The other property that I think is very important is fast tooling / compilation. Compilation speed is not generally the bottleneck right now in agent loops, but models can get faster, and as software scales up and is written by swarms of agents in concert, making the tools run really fast will be an important way to decrease cycle time and increase speed.
[–] norman784 3 days ago
I was thinking about this problem and found a while ago that Unison lang has a cool concept, I recommend you give it a read [0].

- [0] https://www.unison-lang.org/docs/the-big-idea/

[–] empath75 3 days ago
> I strongly believe that there will eventually be a new language created with agents in mind as the primary consumers

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.