# Gallina ## Metadata **Status**:: #x **Zettel**:: #zettel/fleeting **Created**:: [[2026-06-08]] **Topic**:: [[♯ Formal Method]] **Via**:: [[♯ Kleppmann - Designing data-intensive applications]] ## Synopsis ==Proof power and Verified programming== The specification language used in [Rocq](https://rocq-prover.org/). - Dependent types - Implementation generation to Haskell - Better for algorithms and data structures. Slower for distributed system.