We describe preliminary work suggesting that most typing rules for a programming language can be obtained automatically from its operational semantics. Instead of going the usual way, to first define the semantics and the type system, and then show progress and preservation, we start from the semantics and construct a type system that satisfies progress and preservation by construction. We have tested our approach on simple lambda calculi and we have constructed a Haskell prototype that implements our algorithm.