Agda er et afhængigt typisk funktionelt programmeringssprog.Det har induktive familier, dvs. datatyper, der afhænger af værdier, såsom typen af ​​vektorer med en given længde.Det har også parametriserede moduler, mixfix-operatører, Unicode-tegn og et interaktivt Emacs-interface, som kan hjælpe programmereren med at skrive programmet.Agda er en bevisassistent.Det er et interaktivt system til skrivning og kontrol af bevis.Agda er baseret på intuitionistisk type teori, et grundlæggende system for konstruktiv matematik udviklet af den svenske logiker Per Martin-Löf.Det har mange ligheder med andre bevisassistenter baseret på afhængige typer, såsom Coq, Epigram, Matita og NuPRL.