Mathematical proofs of correctness of even simple programs WITHOUT the mentioned technicalities are very complex (multiple times longer than the actual programs). This suggests that there is a lot of inherent complexity in the core software.