I do think that the best way to enforce validation rules is with a logic-paradigm language executed both during compile and run times. That would technically be a dependent type system, but with a bias of allowing runtime verification, instead of trying to prove everything at compile time.