Agda is a dependently typed functional programming language and proof assistant. It allows users to write programs and formalize mathematical proofs in a single framework. Agda's type system enables the expression of complex types, which can depend on values, making it powerful for both programming and verifying correctness. Agda is often used in academic settings for teaching and research in type theory and formal verification. It supports interactive theorem proving, allowing users to construct proofs step-by-step. The language is open-source and has a growing community that contributes to its development and libraries.