I don't think you'll find much use for it when reasoning about a specific computable hash function because there's e.g. no clear distinction between using the p

I don't think you'll find much use for it when reasoning about a specific computable hash function because there's e.g. no clear distinction between using the pingeonhole principle and using the properties of the hash function itself. You could however reason about a 'generic' hash function and show that a particular program can only be broken if someone can find a hash collision. That doesn't really require constructionist reasoning though.