Unless you can teach the compiler how to verify that arbitrary expressions will be true at compile time, you have created a glorified syntax for assert. The reason for the the often strange syntax and structure in functional languages, especially dependently typed ones, is to allow you to restrict how you can construct programs so that it can give you those stronger assurances at compile time. You don't want your program to crash or throw a runtime error when you try to convert an int to a natural, you want it to not be possible to do unsafely in the first place.
> Unless you can teach the compiler how to verify that arbitrary expressions will be true at compile time, you have created a glorified syntax for assert.
Well, right now some languages are able to verify that a variable is non-null at compile time (C#). It should be possible to add range requirements to numeric types (e.g. i > 5), and (non-)equality requirements for most types. Intersections and unions of these requirements is trivial, so the compiler could work out possibly allowed and disallowed value (ranges). If we only allow these simple constraints, it is essentially constraint-solving at compile time. The compiler can "understand" these simple types, and it can see that a positive int (or a non-null Vehicle) is required, and propagate that backwards and see whether it is violated.
(One could go a bit further and add almost arbitrary expressions (of C++11 constexpr strength). If the compiler can't convert the expression to a union or intersection of things it understands, it can still check if a given constant violates the condition. E.g. it is known that x=5, and the precondition of a function is x2 != 25, then this is a violation. I don't know how useful this would be, though. One could also add "lemmas" to aid the compiler, e.g. "I guarantee that x > 10 in this branch".)
