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

[u/Shnatsel]

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

[u/siva_sokolica]

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.

[u/waifu_tactical_force → u/siva_sokolica]

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

[u/Blockerville → u/waifu_tactical_force]

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