Draft:Move (language)

It was created by Meta (formerly Facebook) as the smart contract language for the Diem digital currency (formerly known as Libra).{{Cite web |title=Move {{!}} Diem Documentation |url=https://developers.diem.com/docs/technical-papers/move-paper/ |access-date=2025-02-09 |website=developers.diem.com |language=en}} After the Diem project got discontinued in 2022, the Move language continued to live independently,{{Cite web |date=2024-07-13 |title=Life After Libra: How Facebook’s Failed Cryptocurrency Kicked off a Web3 Movement |url=https://www.ccn.com/news/crypto/libra-facebook-cryptocurrency-move-web3-language/ |access-date=2025-03-07 |website=CCN.com |language=en-US}} now being supported by the Aptos Labs and the Sui Foundation (both founded by former Meta employees involved in Diem){{Citation |title=move-language/move |date=2025-02-09 |url=https://github.com/move-language/move |access-date=2025-02-09 |publisher=The Move Programming Language}}. There are currently two main Move dialacts: Aptos Move{{Cite web |title=Smart Contracts {{!}} Aptos Docs (en) |url=https://aptos.dev/en/build/smart-contracts |access-date=2025-03-07 |website=aptos.dev |language=en}} and Sui Move.{{Cite web |date=2022-07-15 |title=Why We Created Sui Move |url=https://blog.sui.io/why-we-created-sui-move/ |access-date=2025-02-13 |website=The Sui Blog |language=en}}

Move is a resource-oriented language. Resources in Move cannot be copied, but only moved from one owner to another.{{Cite web |last=Team |first=Springworks |date=2019-08-23 |title=Solidity v/s Move v/s Clarity: The Battle of Smart Contract languages. |url=https://www.springworks.in/blog/solidity-move-clarity-the-battle-of-smart-contract-languages/ |access-date=2025-02-22 |website=Springworks Blog |language=en-US}}

Move is currently used by multiple chains, such as Aptos,{{Citation |title=move-language/move-on-aptos |date=2025-02-07 |url=https://github.com/move-language/move-on-aptos |access-date=2025-02-09 |publisher=The Move Programming Language}} Sui,{{Cite web |last=Ehrlich |first=Steven |title=Making A Move On Ethereum |url=https://www.forbes.com/sites/stevenehrlich/2023/07/18/making-a-move-on-ethereum/ |access-date=2025-02-17 |website=Forbes |language=en}} IOTA,{{Citation |title=Move Overview |date= |url=https://docs.iota.org/developer/iota-101/move-overview/ |access-date=2025-03-07 |publisher=IOTA Documentation}} Movement,{{Cite web |last=Manche |first=Cooper Scanlon,Rushi |title=We're Gen Z college dropouts who raised $41.4M for our blockchain startup. Here's how we did it |url=https://fortune.com/2024/08/20/gen-z-tech-entrepreneurs-movement-labs-blockchain-startup-web3-meta-move-programming-language/ |access-date=2025-02-17 |website=Fortune |language=en}} starcoin,{{Cite web |title=The Top Move Programming Language Examples, Explained |url=https://supra.com/academy/the-top-move-programming-language-examples-explained/ |access-date=2025-02-09 |website=supra.com |language=en-US}} 0L. Interoperability with other chains (such as Ethereum or Solana) can be provided through the Lumio abstraction framework.{{Cite web |title=Lumio |url=https://lumio.io/ |access-date=2025-02-22 |website=lumio.io |language=en}}

The Move Prover (MVP){{Cite book |last1=Zhong |first1=Jingyi Emma |title=Computer Aided Verification |last2=Cheang |first2=Kevin |last3=Qadeer |first3=Shaz |last4=Grieskamp |first4=Wolfgang |last5=Blackshear |first5=Sam |last6=Park |first6=Junkil |last7=Zohar |first7=Yoni |last8=Barrett |first8=Clark |last9=Dill |first9=David L. |date=2020 |publisher=Springer International Publishing |isbn=978-3-030-53288-8 |editor-last=Lahiri |editor-first=Shuvendu K. |series=Lecture Notes in Computer Science |volume=12224 |location=Cham |pages=137–150 |language=en |chapter=The Move Prover |doi=10.1007/978-3-030-53288-8_7 |pmc=7363214 |editor2-last=Wang |editor2-first=Chao}}{{Cite web |title=move/language/move-prover/doc/user/spec-lang.md at main · move-language/move |url=https://github.com/move-language/move/blob/main/language/move-prover/doc/user/spec-lang.md |access-date=2025-02-13 |website=GitHub |language=en}} is a tool designed to formally verify smart contracts written in Move. It can automatically validate (or prove the violation of) properties written in the Move Specification Language (MSL).{{Citation |last1=Dill |first1=David |title=Fast and Reliable Formal Verification of Smart Contracts with the Move Prover |date=2022-02-13 |arxiv=2110.08362 |last2=Grieskamp |first2=Wolfgang |last3=Park |first3=Junkil |last4=Qadeer |first4=Shaz |last5=Xu |first5=Meng |last6=Zhong |first6=Emma}}{{Cite web |title=Overview {{!}} Aptos Docs (en) |url=https://aptos.dev/en/build/smart-contracts/prover |access-date=2025-02-13 |website=aptos.dev |language=en}}{{Cite web |title=Verify Smart Contract: Move Prover Tutorials {{!}} Starcoin Cookbook |url=https://cookbook.starcoin.org/docs/move/move-prover/mvp-tutorial/ |access-date=2025-02-13 |website=starcoinorg.github.io |language=en-US}}{{Cite web |date=2020-10-21 |title=Formal verification of Move programs for the Libra blockchain |url=https://www.fields.utoronto.ca/talks/Formal-verification-Move-programs-Libra-blockchain |access-date=2025-02-13 |website=Fields Institute for Research in Mathematical Sciences |language=en}} The Move Prover encodes the Move source code, together with a set of specifications written in MSL, as a mathematical model, which is then translated into the intermediate verification language Boogie,{{Citation |title=boogie-org/boogie |date=2025-02-11 |url=https://github.com/boogie-org/boogie |access-date=2025-02-13 |publisher=Boogie}} and finally verified through SMT solvers.{{Cite web |title=The Move Prover: A Guide |url=https://osec.io/blog/2022-09-16-move-prover/ |access-date=2025-02-13 |website=OtterSec |language=en}}

.

:Category:Programming languages

{{Drafts moved from mainspace|date=February 2025}}

{{Draft categories|:Category:Programming languages

:Category:Domain-specific programming languages

:Category:Statically typed programming languages}}