Hacker News
points by jordan_bonecut 4 days ago | 0 comments
This language has been something I've wanted to build for years. For a while I thought I'd get my PhD and build it there. But now it's very possible to have Claude build it while I'm at work and give it intense code review every day. It's still not in a "useful" place yet, but I'm curious what fellow programmers think of a language like this. If I continue work is this something anyone thinks they'd enjoy using? Would love some feedback, thanks!
[–] sblom 4 days ago
It's a really great concept. What guarantees are made by the prover?

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.

[–] jordan_bonecut 4 days ago
Thanks! The guarantee is that, without the use of trustme (which can prove any fact), you cannot address memory as the wrong type. The compiler also ensures that a pointer/reference to a value is live at compile time, so it’s not possible to create an invalid pointer (without the use of trustme). You can also claim any fact which the compiler must prove in order to continue compilation.

That is good advice, I’m definitely planning on including some batteries soon, once I’m very happy with where the compiler is at.

[–] yunnpp 3 days ago
> You'll either need a killer interop story with an already built ecosystem

On that note: allow me to "import" or "use" a C header without writing any FFI code.

[–] empath75 3 days ago
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.

[–] n_u 3 days ago
This is cool! Thanks for sharing. I've been wanting something like this for a while

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?

[–] ChickeNES 3 days ago
Why optimize for old fashioned manual programming, especially since you are vibe coding the language to begin with? Unless you think Claude and friends will “enjoy” using it more.
[–] jordan_bonecut 3 days ago
Because good tools are good
[–] 0c3ca83 3 days ago
It's so strange how much effort goes into producing a language that people don't even intend to write.
[–] jeremyloy_wt 3 days ago
To me it’s about determinism and feedback. Agents will make mistakes but if they get clear feedback from the tools they use, they will produce a good result.

There are a shrinking number of reasons to geenfield projects with non-strict or unsafe languages now.

[–] gchamonlive 3 days ago
What's strange is only seeing value in manually writing code when clearly AI is very useful to produce quality code here.
[–] 0c3ca83 3 days ago
you can ask ai to write code in existing languages with large training sets, and it'll do better because of the large volume of training data.

if you're all-in on ai, you want to prioritize familiarity for agents.

[–] gchamonlive 3 days ago
The objective of this project isn't to make a language fit for AI to write but to make a "probably safe system language" regardless of who's doing the coding.
[–] ModernMech 3 days ago
That would imply the AI should write every program in Python from now until the end of time; but just because the AI is most familiar with Python doesn’t mean we have to throw everything we know about system design and using the right tools for the job out of the window.
[–] 0c3ca83 3 days ago
Yes, Python or Rust would make sense to use as long as you're planning on sticking with LLMs.
[–] ModernMech 3 days ago
Not in every situation for all time, that's my point. Which language the AI should use will evolve over time as use cases and computing hardware evolve. It isn't the case that language design is now ossified at whatever existed in 2023.

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.

[–] 0c3ca83 3 days ago
> Not in every situation for all time, that's my point.

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.