Dependent types are powerful enough to encode most properties of programs, and an Idris program can prove invariants at compile-time.
Tipurile dependente sunt suficient de puternice pentru a codifica cele mai multe proprietăți ale programelor, iar un program Idris se poate dovedi invarianți în timpul compilării.