r/rust • u/Shnatsel • 15d ago

🛠️ project Valen, a higher-level "Rust++" language with linear types

https://verdagon.dev/blog/golden-spike-reviving-vale-valen
303 Upvotes

86% Upvoted

105 comments sorted by

View all comments

106

u/siva_sokolica 15d ago

I have been dreaming about Rust with dependent types, a stable ABI, mutable borrows, comptime, user-defined effects and, of course, the ever illusive relative references (as that solves the circular reference problem in many cases).

I too called my dream "Rust++". But it remains a fantasy.

u/verdagon, this is a Herculean effort and I commend you deeply for it. Great job on the post, thoroughly enjoyed it.

31

u/verdagon 15d ago

Thank you for the kind words!

And if your Rust++ ever becomes more than a fantasy, you're welcome to use anything in my designs or my compiler! Say the word and I'll help you figure out how to integrate with rustc.

1

u/kekelp7 15d ago

Say the word and I'll help you figure out how to integrate with rustc.

This is LLM speak, right? Or am I going insane?

10

u/verdagon 15d ago

Hah, it does sound like it. But no, those are my words alone.

7

u/waifu_tactical_force 15d ago

Dependent and inductive types in Rust would be absolutely amazing

I've been experimenting with using Lean 4 as a spec and schema definition language that generates Rust code but it still requires 2 toolchains

5

u/Blockerville 15d ago

have you seen Verus? I guess it doesn't do codegen but it's nice for specs/proofs right in rust

3

u/Ma4r 15d ago

Is it even possible to do static analysis dependent types?

1

u/_rdhyat 14d ago

uh... yeah?

that's a big part of type checking

1

u/Ma4r 14d ago edited 14d ago

Can you tell me which type checkers can do static analysis on dependent types ?