Comment by nothrabannosir
21 hours ago
This thread started with:
> Is asserting the assumptions during code execution not standard practice for formally verified code?
Are you using the same definition of "assert" as that post does?
21 hours ago
This thread started with:
> Is asserting the assumptions during code execution not standard practice for formally verified code?
Are you using the same definition of "assert" as that post does?
I'm not clear what definition of assert anyone is using. Thus I'm trying to create a new one that I think is useful (in the context of this type of discussion only!).
Verify means you checked.
Assert means you are suggesting something is true, but might or might not have checked. Sometimes an assert is "too hard" to verify but you have reason to think it is true. This could be because of low level code, or just that it is possible to verify but would cost too much CPU (runtime, or possibly limits of our ability to prove large systems) Sometimes assert is like a Mafia boss (It is true or I'll shoot - it might or might not really be true but nobody is going to argue the point now. This can sometimes be needed to keep a discussion on a more important topic despite the image)
assert in most languages is a boolean that crashes the program if it is false.
If you want to assert that a list is sorted, you need some function that checks if it is sorted and returns a boolean.
In many (most?) languages assert is an optional crash if false. The language can choose to run the check or not. A function to check if a list is sorted and return a boolean is not hard to write - but of course you then need to prove that function is correct.