We implement extraction of Coq programs to functional languages based on MetaCoq’s certified erasure. As part of this, we implement an optimization pass to remove unused arguments of functions and constructors, making integration with the (often polymorphic) extracted code easier. This pass is proven correct over a weak call by value operational semantics that fits well with many functional languages. We argue that our extraction pipeline applies generally to these functional languages with a small trusted computing base of only MetaCoq and the pretty-printers into these languages. We apply this to two functional smart contract languages, Liquidity and Midlang, which are respectively similar to Ocaml and Elm. This is done in the context of the ConCert framework that allows proving properties of functional smart contracts. The extraction is exemplified by several programs, including a smart contract that uses dependent types, showing that we are able to handle non-trivial programs. We also contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. With ConCert’s executable specification our contracts are furthermore fully testable from within Coq. This enables us to integrate property-based testing into ConCert using QuickChick. We show that this is successful by testing complex contracts such as the congress contract (the essence of TheDAO), an escrow contract, an implementation of a Decentralized Finance (DeFi) contract which includes a custom token standard (Tezos FA2), and more. In total, this gives us a way to write dependent programs in Coq, test them semi-automatically, verify them, and then extract them to functional smart contract languages, while retaining a small TCB.