> The ability to prove, in isolation, the relevant properties about some entity (e.g., a function, a hardware module, or what have you), and then to make use of these properties, without ever looking inside the entity again, to prove properties of some larger system, seems to me to be absolutely essential for scaling proofs to large systems.
I understand the motivation, and of course you're right that it would be "essential", it's just that it has been mathematically proven (see my post) that this is not the case. Results in computational complexity theory, that studies how hard it is to do things, show that "making use of these properties, without ever looking inside the entity again" does not, in fact, make verification easier. More precisely, the difficulty of proving a property of A_1 ∘ ... ∘ A_n is not any function of n, because we cannot hide the inner details of the components in a way that would make the effort lower even though that is what we want to do and even though it is essential for success.
In practice, we have not been able to scale proofs to large systems, which means that maybe there is some truth to those mathematical results.
I understand the motivation, and of course you're right that it would be "essential", it's just that it has been mathematically proven (see my post) that this is not the case. Results in computational complexity theory, that studies how hard it is to do things, show that "making use of these properties, without ever looking inside the entity again" does not, in fact, make verification easier. More precisely, the difficulty of proving a property of A_1 ∘ ... ∘ A_n is not any function of n, because we cannot hide the inner details of the components in a way that would make the effort lower even though that is what we want to do and even though it is essential for success.
In practice, we have not been able to scale proofs to large systems, which means that maybe there is some truth to those mathematical results.