Agda هي لغة برمجة وظيفية مكتوبة بشكل صحيح.يحتوي على عائلات استقلالية ، أي أنواع البيانات التي تعتمد على القيم ، مثل نوع المتجهات ذات الطول المحدد.كما أن لديها وحدات نمطية ، مشغلات mixfix ، أحرف Unicode ، واجهة Emacs التفاعلية التي يمكن أن تساعد المبرمج في كتابة البرنامج.اغدا هو مساعد إثبات.إنه نظام تفاعلي للكتابة والتحقق من البراهين.يعتمد Agda على نظرية النوع البديهية ، وهو نظام تأسيسي للرياضيات البنائية التي طورها السويدي بير مارتين لوف.لديها العديد من أوجه التشابه مع مساعدي إثبات آخرين بناءً على أنواع تابعة ، مثل Coq و Epigram و Matita و NuPRL.