YHK - yet another hacker news clone

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.

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

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.

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.

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

The introductory examples look more like refinement type (or Liquid types) which are limited to those operations and restrictions one’s that are provable by the compiler utilizing a restricted subset of operations and computational constructs subject to deterministic proving via SAT solving. I’m going to look closer at the docs so I could be mistaken on that point. It certainly seems to have taken the ownership and ‘borrowing’ concepts for memory semantics from Rust at a quick glance at the first few pages.

I see minor differences; however, the author does nothing to highlight them. That's the number one thing that any new language should show when it's trying to fit into a niche that a language already exists for: What makes this language different?

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

Hard agree. PHP did it right with backslashes.

Any links to the historical reason for C++ using ::?

This is good feedback. I will chew on this…

> It was horrible in C++ from day one, and is still horrible in Rust.

I don't get it. Is it syntactically horrible or are there real reasons that I'm missing?

My favorite namespacing syntax is ironically Clojures. module/func or fully.qualified.module/func or just func if you explicitly import the symbol. I vastly prefer shallow namespacing (module/func) most of the time.

I write Rust mostly for my day job (and it's also my preferred language on the side these days), so I usually end up explicitly importing all the symbols I actually use because module::func is just additional noise in an already pretty verbose language and is what's considered 'idiomatic'.

I don't really get the issue with :: being the separator used here. It's slightly ugly, but it's visually distinct from . for field access, which I do appreciate.

> it looks to me that the authors of those languages are parroting other languages rather than understanding the reason of those language choice.

I don't mean this to sound combative, but I think you are the one who doesn't understand the reason for the language choice. I assume you're objecting to the fact that these languages use different operators for module/namespace paths (`::`) and object member/method access (`.`), not the `::` symbol specifically.

You seem to assume that Rust blindly imitated C++, but that's not the case. The `::` syntax allows the compiler to know which paths can be resolved statically, before type inference and other analysis. This is important because macros are expanded between these stages, and can in turn introduce more static names which must also be resolved before any further compilation.

You might be able to introduce a rule that any `.`-path that can be resolved statically will be, trumping any non-static members (or maybe not, it might cause ambiguities I'm not thinking of), but Rust's design philosophy has always favored explicitness.

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