How close tau language will be to languages such as irdis/agda?
quite same logic/typesystem (Martin-Lof type theory), but the syntax is completely different (namely, semantic web family e.g. NQuads, Turtle, or Notation3)
btw, talking about irdis...
but it all actually misses the most important drawback of ethereum contracts - the need to re-execute the whole contract by each and every participant vs verification of a proof (which is much faster).