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.

▲

jordan_bonecut an hour ago | parent | next [-]

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.

▲

ch4s3 an hour ago | parent [-]

How long have you been working on this?

▲

jordan_bonecut an hour ago | parent [-]

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

	▲	ch4s3 39 minutes ago \| parent [-]
		Oh cool, it's amazing how quickly you can stand up a language now, I love it. I'd love to exchange ideas, I really like what you're doing. How are you doing resolution of your dependent(refined?) types? I've been using Z3, but you're clearly doing something else here.

▲

ch4s3 an hour ago | parent | prev [-]

Yeah it definitely looks like refinement vs actual dependent types. I do the same thing here[1] in my language (pardon the mess). Adding liquid types to basically rust is IMHO a good idea.

[1] https://march-lang.org/docs/refinement-types/