Facebook’s “Move” Programming Language: How Does It Compare to Solidity and DeepSEA?

This report compares Ethereum's Solidity, Facebook's Move, and CertiK's DeepSEA, emphasizing how each language approaches safety and formal verification: Solidity is flexible but error-prone (subject to overflows, re-entrancy, and compiler bugs) and relies on third-party verification; Move restricts expressivity and adds resource types plus a bytecode verifier to be more verification-friendly; DeepSEA integrates formal verification via Coq and a proven compiler to provide stronger correctness guarantees. The analysis concludes that newer languages aim to learn from Solidity's vulnerabilities to produce more secure smart-contract ecosystems.