4 ms·

rank (n) * 8: formal verification of technology of rank n

• freyrs3 14y ago
  I think operating systems are harder to formally verify than programming languages.
• jules 14y ago
  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.
  • dons 14y ago
    Agreed. The more difficult on that list, the more formal the system, and the more automated tools that have been developed to automate verification.