Comment by kg
1 day ago
> Moreover, type systems can track that a list was previously sorted and maintained it's sorted status making the assumption reasonable to state.
This is true, but if you care about correct execution, you would need to re-verify that the list is sorted - bitflips in your DRAM or a buggy piece of code trampling random memory could have de-sorted the list. Then your formally verified application misbehaves even though nothing is wrong with it.
It's also possible to end up with a "sorted" list that isn't actually sorted if your comparison function is buggy, though hopefully you formally verified the comparison function and it's correct.
You already have hardware level bit flip verification, you don't need to recheck the list
That only works up to some level of bit flips, like all error correcting codes. It works for our maybe even two bit flips, but not more than that.
Only if you have ECC RAM, and even then it’s not perfect.