Tau isn't yet complete. OCaml is a good language and there are others but the issue is, no one has built anything similar to an OCaml smart contract language. Tau is actually going through a redesign phase right now but the lead developer has chosen to go with MSO (monadic second order logic) over graphs.
Monadic second-order logic (MSOL) is a restriction of second-order logic in which only quantification over unary relations (i.e.: sets) are allowed. Quantification over functions, owing to the equivalence to relations as described above, is thus also not allowed. The second-order logic without these restrictions is sometimes called full second-order logic to distinguish it from the monadic version. Monadic second-order logic is particularly used in the context of Courcelle's theorem, an algorithmic meta-theorem in graph theory.
I do agree if Tau exists then use it, because coming up with a new language for smart contracts is hard, and to trust any compiler which isn't designed correct by construction is also a mistake.