I have only studied Move by reading the whitepaper, but there's a gaping architectural hole that I found in five minutes:

    public withdraw_from_sender(amount:u64): Coin {
       let transaction_sender_address: address = GetTxnSenderAddress();
       ...
    }

Checking the global txn sender address is not a sound way to authorize a transaction in a smart contract language. Consider that a buggy or malicious function in a different smart contract could call withdraw(). Linear type theory might prevent the resulting stolen coins from being duplicated, but they're still stolen.

I don't know if there is a clean theoretically sound way to do this, but here's an idea based on linear types:

The main function in a transaction is given a Sender object as one of its arguments. The Sender has a method that generates an assertion (an object) that the transaction intends to perform a specific action, e.g. withdraw 10 coins of type A. The withdraw() function takes an assertion as a parameter and calls a method that consumes the assertion before withdrawing the coins.