Verifiable computing (VC) uses cryptography to delegate computation to untrusted workers. But in most VC schemes, the delegated program must first be arithmetized – expressed as a circuit with multiplication and addition over a finite field. Previous work has compiled subsets of languages like C, LLVM, and bespoke assembly to arithmetic circuits. In this paper, we report on a new DSL for VC, called Snaarkl (``Snorkel''), that supports encodings of language features familiar from functional programming such as products, case analysis, and inductive datatypes. We demonstrate that simple constraint-minimization techniques are an effective means of optimizing and solving the resulting encodings, and therefore of generating and constructing witnesses for small circuits.