@kellysmith12.21 they are different precisely because a type system doesn’t work at runtime — that’s what it means to be a type system

@samth is there also another good distinction between types and contracts in that types should always be decidable and terminate in finite time but contracts can possibly express non-terminating arbitrary computations?

@abmclin there are undecidable type systems (lots of them) and type systems with programs in them (ie dependent types). The distinction is really about compile-time vs run-time

thanks for the info!