I'm a little disappointed in the lack of substantive discussion here! There are many interesting technical issues raised by this post ripe for discussion. For instance:
> As you can see from the source files, that required adding many specifications (around 400 preconditions and 500 postconditions) and ghost code (around 150 loop invariants, 400 assertions, 300 ghost entities), and the daily proof takes 1.5 hours on a Linux server with 36 cores.
So 40 units with only a few hundred pre/post conditions and invariants seems to take an enormous amount of compute time to verify.
I expect that the verifier has already been fairly well optimized since Spark has been around awhile. Is this the case?
For verification in general, is the expense of verification in this case because of the model needed to verify Ada? For instance, perhaps a language that makes different choices might have a model checker that could scale better.
This has important implications for scaling formal methods to more software.
> As you can see from the source files, that required adding many specifications (around 400 preconditions and 500 postconditions) and ghost code (around 150 loop invariants, 400 assertions, 300 ghost entities), and the daily proof takes 1.5 hours on a Linux server with 36 cores.
So 40 units with only a few hundred pre/post conditions and invariants seems to take an enormous amount of compute time to verify.
I expect that the verifier has already been fairly well optimized since Spark has been around awhile. Is this the case?
For verification in general, is the expense of verification in this case because of the model needed to verify Ada? For instance, perhaps a language that makes different choices might have a model checker that could scale better.
This has important implications for scaling formal methods to more software.