What kind of bug can resource data model avoid?

The code of withdraw procedure in LibraCoin.mvir is blow:

    public withdraw(coin_ref: &mut Self.T, amount: u64): Self.T {
        let value: u64;

        // Check that `amount` is less than the coin's value
        value = *(&mut copy(coin_ref).value);
        assert(copy(value) >= copy(amount), 10);

        // Split the coin
        *(&mut move(coin_ref).value) = move(value) - copy(amount);
        return T{value: move(amount)};
    }

As the third line from the bottom shown, the procedure changes the value of origin resource by a subtraction. If a careless programmer write a wrong implementation, such as *(&mut move(coin_ref).value) = move(value) - copy(amount) - 1;, causing an incorrect total amount of resource Coin. Obviously, resource data model can’t avoid such mistake, so I wonder what kind of bug can resource data model avoid?

Here is what the Move paper says on this:

We note that the Move type system cannot catch all implementation mistakes inside the module. For example, the type system will not ensure that the total value of all Coins in existence is preserved by a call to deposit. If the programmer made the mistake of writing *move(coin_value_ref) = 1 + move(coin_value) + move(to_deposit_value) on the final line, the type system would accept the code without question. This suggests a clear division of responsibilities: it is the programmer’s job to establish proper safety invariants for Coin inside the confines of the module, and it is the type system’s job to ensure that clients of Coin outside the module cannot violate these invariants.

Said differently: the resource safety guarantees should be viewed as protection from buggy or malicious clients of some module M. If the author of M can enforce some local invariants on its declared types, the type system will ensure that these are local invariants are also global invariants. But if M fails to enforce those invariants, the type system can’t help (because it doesn’t know what invariants the module author is trying to enforce!).

Because of Move’s resource types, these invariants can include guarantees that are difficult or impossible to enforce in a conventional language. One example is privileged destruction: a Move module can enforce an invariant like "type T can only be destroyed if expression e evaluates to true". Conventional languages don’t make it possible to set preconditions on the destruction of a type.

1 Like

Thanks for explanation!