@milo the curry style lambda calculus:

multiplicity of type checker implementations for the same type system (rigorously defined) like ... might save you development time, but it's not a super compelling idea. if the type system isn't well defined then this becomes an even weaker proposition. if the type system isn't defined and leaves lots of decisions up to the implementation then it becomes a straight up bad idea