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 2 hours ago | parent | next [-]

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 2 hours ago \| parent [-]
		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.

▲

empath75 18 minutes ago | parent | prev | next [-]

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.

▲

0c3ca83 an hour ago | parent | prev [-]

It's so strange how much effort goes into producing a language that people don't even intend to write.

▲

jeremyloy_wt an hour ago | parent | next [-]

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 an hour ago | parent | prev [-]

What's strange is only seeing value in manually writing code when clearly AI is very useful to produce quality code here.

▲

0c3ca83 39 minutes ago | parent [-]

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 36 minutes ago \| parent [-]
		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.