>This seems orthogonal to me. If you allow pointers, then linear types don't help you either, right?

Unsafe pointers should exist at the FFI boundary and be wrapped in a linear API. Every language has a "escape hatch" for this purpose, and you ultimately have to rely on practices to constrain it. You can call malloc in any language.

>But if the compiler can verify that a value is used exactly once, then why can't it verify that a value is destructed? We mark a function as a destructor and the compiler verifies that the value is passed to a destructor exactly once.

The problem is the compiler can't verify it. In a Turing complete language, it's simply impossible to do it in a general way without restrictions. Every language that has compile time memory safety (Austral, Rust, Cyclone, a few others) imposes restrictions to make the analysis tractable.

>I'm probably missing this, but this also seems orthogonal. It seems like Capabilities are implemented with different types. The Filesystem type is different from the Path type, and you get different capabilities depending on which type you get. This has nothing to do with linear types.

Capabilities have to be linear so that they can't be copied surreptitiously:

https://austral-lang.org/spec/spec.html#rationale-cap

>I'd like to know more about this, because it sounds cool.

There's some examples in the post. The state machine is the state of the file handle and the linear types ensure only valid transitions can be used.

>This also sounds cool. Do you have a code example off the top of your head?

Not something existing I can point to. But if you have a function:

    generic [T: Type]
    function reverse(list: List[T]): List[T]

If `List` is linear then this can use in place reversal while the interface is referentially transparent. Because for the type system, the list that goes in is consumed, and cannot be used again, and the list that comes out is a brand new linear type. It just happens to use the same storage.

There are uses for unsafe pointers beyond FFI. In fact, it's only feasible to prove that unsafe pointers are used soundly if the unsafety is contained within a well-defined program module. (Proper inter-module 'FFI' with unsafe pointers would need something like full separation logic, which is very complicated!)

Thank you--super helpful.

"But if the compiler can verify that a value is used exactly once, then why can't it verify that a value is destructed? We mark a function as a destructor and the compiler verifies that the value is passed to a destructor exactly once."

Even when you could verify this, it wouldn't prevent use after free bugs.

UAF are solved by an affine type system (like Rust has), they don't require a linear type system.

That is, an implicitly invoked destructor is not an UAF concern.

Agreed. To be clear, I'm not explaining why the OP chose linear types over affine types (I have mixed feelings on choosing one or the other) but rather why one needs either affine or linear types rather than "disposed exactly once" types.

Thank you--yes, that makes sense.