> At least in some languages this is not an issue if one is able to use higher order functions, with bonus points if they allow for trailing lambdas.

I am afraid you are talking nonsense. Higher-order functions make verification harder, not easier, because they hide the point at which control flow is transferred from one module to another. This is backwards, because this point should be prominent, in big neon letters, precisely so that you can tell exactly when a resource stops being available, or when an invariant goes from being “your responsibility” to “someone else's problem”.

I think pjmpl is referencing apis like this:

   with_file "hello.txt" (fun fd -> (* do stuff *) )

where you've basically created a c++ destructor style api with a lambda.

It's certainly not "verification" in any formal sense, and the type system can't help you there any more than it can in c++.

But this is a perfectly reasonable pattern.

> where you've basically created a c++ destructor style api with a lambda.

Except for the part where destructors are meant to be called no more than once per object, at the end of its lifetime. All that you can guarantee is that `with_file` doesn't call the destructor more than once. But that's not terribly interesting.

You can screw up destructors in exactly the same ways. And it also serves to make sure you close the file at all.

But again hence the value of having the lifetime of the object enforced by the type system.

In the presence of reference-counted mutable objects, destructors no longer guarantee that cleanup will happen. But that much is okay. This is a liveness property, and, as far as I can tell, nobody really knows of any non-annoying way to enforce liveness properties with types. On the other hand, “cleanup is the last operation that can be performed on an object” is a safety property, and types are excellent tools for verifying properties of this kind.

Yep, that was it. Thanks for the example.