agda

Agda is a dependently typed programming language. PLEASE REPORT ISSUES AT https://github.com/agda/agda/issues !

Dependent types allows more properties of programs to be expressed in the types. Not only does this give stronger guarantees that the program is correct, stronger types also helps in the process of writing the program.