Dependent types and things like that are probably great. Being able to prove correctness is great. But I would settle for a way to declaratively express invariants and then let the language for the most part take care of inserting checks (in debug or using a special mode perhaps, or all the time) and generating tests/property tests. Why isn’t this more of a thing?
Because that's a half-assed way of using and leveraging a good type system? DBC always strikes me as a "three blind men and a type system worth using" parable.
Languages like Dafny and Ada show that you can contracts are great for augmenting a good type system by letting you express really complicated invariants that are tough to express in types. I didn't include them because they're not "mainstream", IMO.
Dependent types are extremely difficult to use in practice for non-experts, and more or less don't work at all on floating-point numbers. Idris and a few other languages are working on it, but I think we are a long way off from there. Dynamic contracts solve the problem well enough for most use cases, even if they don't solve it fully.
To my mind contracts only complement a type system. I might want to effectively assert that a function returns a sorted list but I don’t want to assume it is true just based on the assertion never failing; I don’t want the sorted property to be reflected in the type.
A type that proves that all values that inhabit it are sorted would also be nice. But if either the language doesn’t support dependent types or it is too difficult to prove then a contract could be used instead (again: not as a replacement).
So to my mind (repeating idiom) it can work paralell to the type system. What’s not to like (honest question :))? It doesn’t have to be intrusive, as far as I can see.
> A type that proves that all values that inhabit it are sorted would also be nice. But if either the language doesn’t support dependent types or it is too difficult to prove then a contract could be used instead (again: not as a replacement).
This is really easy in a dependently typed language. If something is hard to prove by construction you can do
sort: List -> List
which sorts a list without proving it to be sorted, and then write a function
isSorted: List -> Maybe SortedList
then just get your safe sort function
safeSort: List -> SortedList
safeSort l = case sort l of { Nothing -> panic; Just x -> x }
Of course, you don't even need dependent typing to do this. If SortedList is a new nominal type and you trust your issorted function, everything works out.
The not-so-easy part arises when you need to operate on a SortedList and want to enforce that it remains sorted after said operation. Maybe in the specific case of SortedList it's not that bad, but my (limited) experience is that the complexity in such cases can accumulate surprisingly high and surprisingly quickly.
I have frequently found myself out of my depth when trying to write what I thought should be straightforward dependently-typed code. I got the hang of it after a lot of practice (as well as a lot of reading, note-taking, and outside help). But now you're asking programmers to learn an entirely new set of skills on top of everything else they're expected to know.
I love the idea of dependent types, and I've had a lot of fun messing around with Idris 2, but I think dependently-typed languages have a lot of work to do in order to bridge the ergonomics gap.
I'm not convinced that, for garden-variety software development, dependent types are substantially safer than extensive use of contracts and property-based testing.
That's exactly what my framework does. As long as you're okay with runtime panics (which would happen anyway in a non-dependently typed language), you just have any function you don't know how to prove go from SortedList -> List. Then you have a check List -> Maybe SortedList. And finally a function with a panic that lets you write the SortedList -> SortedList version.
This is adjacent to one of my main complaints with Racket's contracts. If I want to use Typed Racket (which I almost always do) then it becomes significantly more difficult to attach non-type contracts to code. I find I often run into cases where I want to encode something as a contract that is impossible to describe with refinement types. Especially when gradually typing an old untyped codebase.
Dependent types and things like that are probably great. Being able to prove correctness is great. But I would settle for a way to declaratively express invariants and then let the language for the most part take care of inserting checks (in debug or using a special mode perhaps, or all the time) and generating tests/property tests. Why isn’t this more of a thing?