you can put arbitrary functions in a contract. with static typing that requires dependent types. and while i'm a fan, that's an enormous can of complexity to bust open.

say you've got a function that takes a list of numbers, and some bounds, and gives you back a number from the list that is within the bounds (and maybe meets other criteria, whatever). your contract for the function could require not only that the list be comprised of numbers, and the bounds are numeric, but also that the lower bound is <= the upper bound, and that the return value was actually present in the input list.