For some types of security, a proof of correctness could be used. (This proof could be machine verified) This would be expensive ( in time and effort spent), b

For some types of security, a proof of correctness could be used. (This proof could be machine verified) This would be expensive ( in time and effort spent), but is possible for some things. With things like crypto though, AFAIK most crypto is based on certain assumptions which seem to be true, even after a high degree of investigation, but for which a proof has not been found. In these cases, it would not be feasible to prove the program to be "secure", but one could prove that the program correctly implements the algorithm. But then there's also timing attacks and the like, and I don't know that there are tools for proving things about the running time of a program, so as to prove that the running time doesn't leak information? But for some things, one can trust a program to be correct if it contains a proof that it is correct, and you agree with what correct is being chosen to mean.