A workshopon az Agda programozási nyelvvel ismerkedünk meg, amelynek fő jellegzetessége, hogy programozási tevékenység definíció + tétel + bizonyítás jellegű.
Például, az legnagyobb közös osztó kiszámolását úgy tudjuk benne leprogramozni, hogy definiáljuk a legnagyobb közös osztót (matematikai értelemben), majd bebizonyítjuk hogy bármely két számnak létezik legnagyobb közös osztója. Az Agda fordító ebből a bizonyításból készít algoritmust. Az algoritmus gyosasága a bizonyítás módjától függ. A kapott algoritmus helyessége a bizonyítás helyességéből következik, amit a fordító ellenőriz.
Ez talán nehézkesebbnek tűnik, mint a hagyományos programozási tevékenység (definíció + tesztelés), de cserébe kevesebb hiba marad a programban.