Tezos seems to have a lot of common points with Tau.
@arthurb: can you confirm if the core language is total functional and if it remains expressive enough to perform more general programming? If it's not, how do you prove mathematically that core protocol operations will always be well behaved and terminate for all input sets?