jordan_bonecut

I’ll look into this

I’m not quite sure I understand your question. But if x is a vector of things that contain allocations, the compiler will track a plane for them and represent them sparsely as needed be.

I agree with you, if I were asking for a code review. I'm mostly interested in what people think of the language features. A code review in its current state is not interesting, but I believe the site has some ideas that can be food-for-thought

Because good tools are good

It is different because for many cases you may need to prove your assertions. Consider:

fn foo(x: usize) -> NonZero where x != 5 { NonZero::new(x - 5) }

I do not believe this is achievable in Rust.

Correct, every allocation is its own plane. The nice thing about this model is that you don't need to explicitly call out lifetimes. I also believe that lifetimes aren't really a good model of what actually happens in memory. This model is more powerful because it understands relationships between planes in memory, which Rust's model doesn't. This is why it requires mutable borrows to be unique which is oftentimes overly restrictive. For instance this is not valid Rust:

let x = vec![1, 2, 3]; let a = &mut x[0]; let b = &mut x[1]; swap(a, b);

Because Rust doesn't really know the difference between the whole Vec an element within the vec. Therefore it treats any mutation as one that could potentially invalidate anything with the same lifetime and doesn't compile. So I believe the plane model to be strictly better because it allows for this and still prevents the real scary thing:

let x = vec![1, 2]; let a = &mut x[0]; x.push(3); a = a + 1;

For me part of the fun of such a side project is complete control. I’m willing to risk this over starting from something existing, which may be the wrong call!

I considered waiting longer to share more but felt feedback early was better than waiting for more polish. Will focus on this with high priority though, good feedback

If you want to assume that overflow wraps either:

Your hardware does this OR You implement it in software

Overflow is allowed. Overflow behavior is unspecified, like C++

That, sir, is a hot take

A compare and contrast is good feedback, will work on this

Another thing - when a value is moved or dropped the plane’s type changes from T to shape(T). shape(T) contains unspecified data but has the size and alignment of a T. So you couldn’t safely prove that a moved out/dropped shape(T) is a T

This is good feedback. I will chew on this…

What I’ve showcased is definitely not full fledged dependent types. Support is planned via ideal generics but it’s lower on the priority list to nail down

The compiler tracks all of the currently living planes. The compiler tracks from which plane each borrow is borrowed. Once the plane it is borrowed from dies that borrow is no longer valid

Allocations live in their own plane, the root allocated typed being the root node of that plane. For threads, I’m still working on that, don’t have a super cool answer yet

And, to be clear, the README was mostly an initial prompt for the AI. I’ll prioritize making a much clearer and legible README soon

I have been building little prototype languages for years. This iteration which is heavily AI powered is a couple weeks old

The compiler statically tracks “where” everything lives. It also knows “when” the “where” is valid.

Each “where” is called a plane, which is a tree. The stack plane contains all your function calls memory, a structure allocated on the stack has a child plane for each field. The compiler tags which plane something is from at compile time and tracks when it dies.

Things do get complicated in scenarios like:

fn max(a: &usize, b: &usize) -> &usize {

  if *a > *b { a } else { b }

}

In such a scenario the compiler tags the result with both of the input planes. However, you cannot define add a postcondition ensures clause to make it more precise

Dependent types can be achieved via “ideal Generics”. Very undocumented and not ready to commit to how they work yet, but the basic idea is that a type can be generic on a value.

Yeah the repo/documentation is pretty rough right now. TBH I am not quite ready to spend a ton of time on docs yet as some of these things are changing on the fly. But the core concept/syntax should remain the same. The code is not super interesting yet, though

Dependent types are part of it, yeah! There are definitely some things I dislike about Rust which I am not planning on including, mainly lifetimes and some ways they handle pointer mutability. One thing I particularly dislike about Rust is:

let x = vec![1,2,3]; let a = &mut x[0]; let b = &mut x[1]; swap(a, b);

This is not allowed. And actually in the compiler’s mind it’s for the same reason as this:

let x = vec![1,2]; let a = &mut x[0]; x.push(3); a = a + 1;

Which is definitely not safe and should be rejected. But the compiler cannot reason that the above case is actually safe, because they both fail to compile for lifetime reasons.

Another thing I’m working on are “patterns” which are like enums on steroids. In Rust you cannot define how an enum is laid out, thus requiring optimizations for types like Option<&T> to be in the compiler. In evergreen this will be in the language via a similar process to trait implementation.

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.

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!

Go is an incredible programming language - but many people want a couple of things: 1. Tagged union types 2. An early return operator

Luckily LLMs are quite good at these surgical changes. In fact I only used ~10% of my weekly limit on Codex (granted, I have the $100/mo plan) and a few iterations of review to implement them. I wouldn't go and use them in production in their current state but it's fascinating to see just how easy it is to add these features in a workable manner to projects as large as Go.

A little info on how each of the features work:

1. Tagged unions: These are compiled down to a struct with a series of 0-length arrays of each of the union field types. This enforces proper alignment. There is a byte array which is as long as the longest subfield where the payload lives. There is also an 8, 16, 32, or 64 bit variant field for distinguishing the active variant. Finally there is a "gc anchor" (codex's naming) which is a pointer to information for the gc to properly collect the active field. While this field is technically redundant, implementing unions without it would require a significant change to gc. Ideally I'd like to keep this fork (if I choose to maintain it) more or less in sync with master so I've decided not to do this for now.

2. Early return with "!": In a multi-value context if the final value is of type error I can use the special "!" bang operator. I can only use this operator if the current function I'm in has its final return type as an error. If both of these condition are met the bang operator will early-return from the surrounding function if the final value of the multi-value context is a non-nil error. This reduces a lot of "if err != nil" boilerplate.

Finally I asked the LLM to refactor the go source to use these two new constructs on this branch (https://github.com/jordan-bonecutter/go-plus-plus/pull/3). I haven't looked much at this branch myself but it easily (within about an hour) removed 5k+ lines of code from the go source. It also found some real bugs, like a potentially nil error value being returned in some plan9 code. Anyways, check it out and let me know what you think. Useful? Garbage? Thanks!

Disagree, there are practical trivial subsets of the halting problem to which I imagine many short-running scripts would conform.

Yes, but it could learn to associate tokens with word counts as it could with meanings.

Even still, if you ask it for token count it would still fail. My point is that it can’t count, the circuitry required to do so seems absent in these models

Yes, but so is telling if a photo contains a dog or understanding sentiment in a paragraph of text. Complexity isn't quite the issue, I think it is that there is a distinction between the type of reasoning which these models have learnt and that which is necessary for concrete mathematical reasoning.

This is an interesting article and goes along with how I understand how such models interpret input data. I'm not sure I would characterize the results as blurry vision, but maybe an inability to process what they see in a concrete manner.

All the LLMs and multi-modal models I've seen lack concrete reasoning. For instance, ask ChatGPT to perform 2 tasks, to summarize a chunk of text and to count how many words are in this chunk. ChatGPT will do a very good job summarizing the text and an awful job at counting the words. ChatGPT and all the transformer based models I've seen fail at similar concrete/mathematical reasoning tasks. This is the core problem of creating AGI and it generally seems like no one has made any progress towards synthesizing something with both a high and low level of intelligence.

My (unproven and probably incorrect) theory is that under the hood these networks lack information processing loops which make recursive tasks, like solving a math problem, very difficult.