Na konci prázdnin se bude konat setkání vývojářů jazyka Idris. Jedná se o jazyk pro kritické aplikace s důrazem na bezpečnost a spolehlivost kódu. Formální verifikace například zajištuje v době překladu absenci všech běhových chyb.
Idris je zástupcem totálního funkcionálního programování, tzn. překladač garantuje, že běh všech funkcí vždy skončí. Nabízí několik backendů, mezi jinými C, Scheme, JavaScript nebo JVM.