I will recall the notion of computability introduced by W. W. Tait and J.-Y. Girard for proving the termination of beta-reduction in typed lambda-calculi, and show how it can be extended to deal with various forms of higher-order rewrite relations, and how it can be related with other notions or techniques too.