| > - how much of the burden of writing the proof falls on me, and how much falls to the compiler? The compiler in Idris can do some magic, but usually the burden is mostly on you to write proofs. Idris (and similar languages) have assistance in editors to help you automatically write code and proofs. > What are the full range of things I can express? Dependent types as present in Idris, Coq, Agda, etc. can serve as a foundation for mathematics, so… pretty much anything! For your example, most such languages don't have quotient types, so you'll still need to use setoids or similar to model quotients. > - how huch more effort falls to me when structuring my code, in order to pass the properties or proofs through? It's pretty much the same situation as Haskell or Rust, but I think having to write fromJust / unwrap is great. It tells you when you're reading the code exactly what assumption has been made, and it doesn't seem awfully burdensome. > yet for programming I have to front-load all this complexity to express something so utterly trivial. What's "all this complexity" that you're referring to? |