# Gallina ## 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.