[Yoric]

> What exactly do you mean? How does it differ from any other language's type system?

If you're familiar with affine types, this is basically what Rust's borrow checker implements.

If you're not familiar, it's a bit complicated to summarize on Hacker News. You should try it out, because it lets you guarantee statically entire classes of properties that non-academic languages struggle with.

> In Ada/SPARK, you can formally verify tasks, too. Please take a look at https://docs.adacore.com/spark2014-docs/html/ug/en/source/co.... if you have some time!

I'm not an expert in Ada, but yes, that's pretty similar to some of the properties Rust will let you check out of the box.

edit My memory of Ada was incorrect.

[Manishearth]

It's more than just affine types, it's region typing, which is far less common.

[Yoric]

Fair enough.