Move is a language originally designed for programming Diem (https://github.com/diem/diem), a peer-to-peer network for replicated computation (also known as a blockchain in some circles). The Move programming framework provides: (1) a compiler that lowers the code to bytecode, (2) a verifier that guarantees type and memory safety even in the presence of untrusted code, and (3) a prover capable of verifying functional correctness of compiled bytecode against deep safety specifications. This talk will provide an overview of the language, the bytecode verifier, and the prover. If time permits, I will speculate on new applications for Move.