Programok helyessége
A nyelv koncepciója szerint a függvények típusának kell arról gondoskodnia, hogy a program helyes legyen. Egyrészt a függő típusok használatával nagyjából már kifejezhetjük azt, mit kell egy függvénynek csinálnia, másrészt pedig kijelentéseket, állításokat helyezhetünk a típusba, amelyeknek teljesülnie kell. Az ilyen kijelentéseket mindig bizonyítanunk kell (például az interaktív helyességbizonyító segítségével). A bizonyítások maguk is függvények.
Tételbizonyítás
Az Idris interpreter tartalmaz egy interaktív bizonyítót is, mellyel különböző tételeket láthatunk be. Ezeket aztán felhasználhatjuk programjaink típushelyességének bizonyítására, például előállhat az a helyzet, hogy a típusellenőrző nem képes belátni egy fügvény típushelyességét, és nekünk kell "kisegítenünk" manuális bizonyításokkal.
Ha egy programról tudjuk, hogy az típushelyes, de nem fordul le, helyettesítsük a fordító által hibásnak ítélt részt "ideiglenes definícióval" (= helyett ?=). Ilyenkor az Idris elhelyez egy lyukat (amelyet majd "fel kell töltenünk" saját bizonyítással), és átugorja a problémát. A lyukaknál adódó bizonyítandó állítás belátásához taktikákat használhatunk, melyek előre definiáltak. Pár példa:
- intro - feltételezés felvétele
- rewrite - átírás
- compute - kifejezés kiszámítása
- trivial - vegye észre, hogy két kifejezés azonos
Ha azt szeretnénk, hogy az Idris lásson be valamit anélkül, hogy pontos bizonyítást tudnánk adni, vagyis tulajdonképpen fogadja el, hogy az adott állítást egyszerűen el kell hinnie, használhatjuk a believe_me függvényt. Ez nagyon veszélyes is lehet, mindenképpen csak az átgondolt használata javasolt.