Scientific codes are much harder to verify formally than programming language implementations. Even getting an informal error bound is virtually impossible in m

Scientific codes are much harder to verify formally than programming language implementations. Even getting an informal error bound is virtually impossible in most cases. Formally verifying e.g. web applications is also incredibly hard, but in other ways: (1) it's hard or impossible to formally specify in a non-trivial way (2) the implementation depends on a huge amount of code that needs to be verified or at least specified (OS, compiler, network, etc.). In fact in this list, the most difficult things are the easiest to formally verify: programming language implementations, network stack, OS, filesystems, algorithms, etc.