Is Dependent Types the Best Option?

Ocamel programmers are in some sense spoiled. They're used to the fact that there's a large class of errors that the type system just automatically captures for them. But when you start doing these kind of encoding tricks to add extra rules into the type system, they end up being kind of free-floating and it's very easy to just screw it up. You think you've encoded some permissioning thing correctly and you could just get it wrong. And it's very hard to notice that you got it wrong. It sounds like having something that's kind of more organized around dependent types would ground this kind of coding. So it'd be less likely to just be wrong in a silent