The annotated version of C# included in the blog post reminds me of Spec# http://research.microsoft.com/en-us/projects/specsharp/

Spec# has annotations and methods for object ownership. You can see an example of it in the "The Spec# Programming System: An Overview" slideshow (slide 39 onwards).

Also:

> C# has two families of data structures that dermine allocation behaviour: structs and classes. If a type is a struct then values of that type will be allocated on the stack:

Here's a primer on how the Microsoft CLR handles it, because it's more subtle than what's stated above. The end effect is that value types behave like values, reference types behave like references. Where they're stored is a function of where they need to be stored, not their type.

https://blogs.msdn.microsoft.com/ericlippert/2010/09/30/the-...