Dependent Programming

What Is Dependent Programming ??

Writing a correct computer program is hard and proving that a program is correct is even harder. Dependent Types allow us to write programs and know they are correct before running them.
Dependent types: you can specify types that can check the value of your variables at compile time. A function has dependent type if the type of a function's result depends on the VALUE of its argument; this is not the same thing as a ParameterizedType. The second order lambda calculus possesses functions with dependent types.