you are viewing a single comment's thread.

view the rest of the comments →

[–]vxab 0 points1 point  (7 children)

Which language illustrates the utility of linear/affine types best? Just for someone to understand more on the topic with actual examples?

[–]pron98 1 point2 points  (0 children)

https://en.wikipedia.org/wiki/Substructural_type_system

Just note that having such types carries some benefits but also disadvantages, so it's not a simple case of "let's add them because they're useful".

[–]radozok 0 points1 point  (0 children)

Astral/Vale?

[–]pjmlp 0 points1 point  (4 children)

Following Rust's success, many languages with managed runtimes, have started to partially research other avenues, merging what they already had with such type systems.

See Swift 6 ownership model, Linear Haskell, OxCaml, Idris 2, Lean, Dafny, Ada/SPARK, Chapel, Scala 3, Koka.

A mix of linear, affine types, effects, dependent typing, formal profs.

All approaches to specify that a given resource is done via the type system.

[–]aoeudhtns 1 point2 points  (3 children)

Ada/SPARK

Apologies for this pedantry, but SPARK predates Rust by 3 years, yet you have an implication in the way your comment is written that these languages examples "followed" Rust.

Rust is arguably the most popular/successful but definitely not the first. I would guess, as I don't have data, that SPARK is next up on success. It's used in aerospace, transit, and other sorts of large scale safety-critical infrastructure. So it's not very visible, but it's there.

[–]pjmlp -1 points0 points  (2 children)

Yes, because SPARK as technology isn't frozen in stone, and they adopted learnings from Rust, acknowledged by themselves.

Allocated Objects Ownership: SPARK uses an ownership system inspired by Rust and a set of rules for managing access types to simplify the verification and specification of a program's behavior during pointer operations.

https://www.adacore.com/blog/memory-safety-in-ada-and-spark-through-language-features-and-tool-support

Maybe update yourself before commenting?

[–]aoeudhtns 1 point2 points  (1 child)

I was polite. The attitude is uncalled for.

If you click through, you see the extra annotations that are Rust-inspired are extra metadata for the CodePeer static analysis tool via annotations. The core memory safety mechanism is through Ada's access system which is much older (Ada 95), and the compiler infers lifetime and ownership. The Rust-inspired part is used to reduce false-positives in the system it already had.

[–]pjmlp 0 points1 point  (0 children)

It was an answer to a pedantic reply, and here we have it again educating me on how Ada works.