4 ms·
Type signatures can completely encode specifications in systems with dependent types. Of course no mainstream programming language supports dependent types, but
by curryhoward 11y ago
Type signatures can completely encode specifications in systems with dependent types. Of course no mainstream programming language supports dependent types, but it's worth pointing out that in principle a type can encode any property checked by a unit test. Actually, dependent types are strictly more powerful, since you can prove undecidable properties which can't be checked by unit tests (e.g., that a function does the right thing for all possible inputs).