> The hard part is forming the model. Once you actually know how it's supposed to work, proving it is the easy part. But I mean, how would you even explain to another human that a given algorithm is safe, if not by arguments along the line of "look, this function owns this piece of data and this function owns this piece of data and they're called one after the other"?

One example of how this could work is writing a spinlock. Let's use a made up language for now and adapt that to our need.

alias lock unsigned int;
lock() make_lock (
return 0;
)

void(ref<lock> l) take_lock (
while (l != 0); // Assume this is atomic for brevity
l += 1;
)

void(ref<lock> l) give_lock (
l -= 1;
)

This is a "correctish" non-reentrant lock. This has many vectors to see if this is "correct" from a compiler standpoint. The first is that only the alias "lock" can be passed to my lock even though it is just an "unsigned int". Another mode is that I am doing (lock -= 1). Since this is unsigned if my program ever gets into a state where I am doing (0 - 1) in unsigned arithmatic then I am going to wrap around to UInt.MAX_VALUE which is not how subtraction should behave and it should warn me when this situation arises. If the language allows me I can also do this to help the compiler know that I never want this to happen.

void(ref<lock> l) where (l != 0) give_lock (
l -= 1;
)

Now the compiler can see I absolutly do not want this wraparound behavior and it can check for it. Where would this be the case?

int() thread_safe_fac(ref<lock> l, int some_important_data) (
int f;
take_lock(l);
if (some_importand_data) {
f = some_important_data * thread_safe_fac(l, some_important_data - 1);
} else {
f = 1;
give_lock(l);
}
give_lock(l);
return f;
)

void() main (
lock l = make_lock();
int some_important_data = 10;

some_important_data = thread_safe_fac(&l, 10);

print(some_important_data);
)

Will this code work? Absolutly not and it's easily checkable. One of my function's invariants is violated. give_lock() will sometimes fall negative. This is a very crude example but I've seen code like this in larger projects where someone modified some code and someone refactored that then someone was contracted to add a feature. It just goes down the shitter. But this is easily provablely wrong.

* Call thread safe fac
* grab a lock
* we theoretically touch some thread safe data
* We hit a case where we do an if
* Then run the then case
* else set a default and free our lock
* Free our lock

We've free'd twice and we've now broken the underyling data of the `lock` type. We've got an unsigned int that has been wrapped around to an huge number and take_lock(l) will never work again. Lock is a mutable datatype that can be shared between N many threads/fucntions and it can always be checked like this just by telling the compiler "hey I never want to let the internal int fall into a state where it is subtracting 1 from 0".

This can also be extended to other things

void test(int *num) { *num *= 10; }
int some_complex_function(int *num) {... free(num) ... }

int main() {
int *some_cool_data = (int*) malloc(sizeof(int);
*some_cool_data = 5;

while (true) {
...
test(some_cool_data);
...
some_complex_function(some_cool_data);
...
}
}

We've come to a place in the code where we have a possible path of execution (regardless of the depth in if statments or gotos or other control flow) where we will eventually come to the point where we use a bit of data after it's free'd. This code will be correct if you do something like.

// We now make sure the compiler knows that we only want to accept real references to initialize ptr
int some_complex_function(int **num) where (num && *num) {... free(*num); *num = NULL; ... }

// We've removed the path through the program that allows the data to be used after free.
while (some_cool_data) {
...
some_complex_function(&some_cool_data);
...
}

Again another bad example but there is a lot of perfectly valid, and very clean code that is against the borrow checker but is still completely correct.