Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)?
> Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and then be verified at compiler-time.
What program properties are useful to capture and what properties you can mostly automate is a really interesting problem.
Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be:
(* clearly eqtypes *)
datatype Color = R' | B'
datatype Nat = Z | S : Nat -> Nat
datatype Tree =
| Empty : Tree (B', Z, 'a)
| R : Tree (B', 'h, 'a) * 'a * Tree (B', 'h, 'a) -> Tree (R', 'h, 'a)
| B : Tree ('c, 'h, 'a) * 'a * Tree ('c, 'h, 'a) -> Tree (B', S 'h, 'a)
Only kidding! It stands for Satisfiability Modulo Theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
“In computer science and mathematical logic, the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.”
I'm not sure I'm any the wiser after that …
A notable building block appears to be SMT-LIB http://smtlib.cs.uiowa.edu/index.shtml
Drop in to #dependent on Freenode IRC, and let’s chat.