> Using "length of the correctness statement + length of its proof" works quite well as proxy for complexity of a component (the longer, the more complex).

It sounds like a reasonable concept, but then Principia Mathematica takes 300 pages to prove that 1+1 is 2.