Making it easier to write correct programs
Dependently-typed programming languages, such as Idris and Agda, permit the use of logical properties to constrain the values an expression could take. This allows us to incorporate the proof that a program satisfies…