I think it very much depends on the domain. For instance, I've seen specs for floating point ops that were 1-3 pages compared to 30,000 lines of RTL. That holds pretty well for many other cases. For example, a properties like decompress(compress(x)) = x are beautifully simple compared to the details of the algorithms, and are pretty compelling correctness evidence.