ASSERTING the list is sorted as an assumption is significantly different form VERIFYING that the list is sorted before executing the search. Moreover, type systems can track that a list was previously sorted and maintained it's sorted status making the assumption reasonable to state.

▲

jojomodding 15 hours ago | parent | next [-]

What do you mean when you say "assert" and "verify"? In my head, given the context of this thread and the comment you're replying to, they can both only mean "add an `if not sorted then abort()`."

But you make some sort of distinction here.

▲

bluGill 15 hours ago | parent [-]

Verify means you check. Assert means you say it is, but might or might not check.

▲

cyphar 14 hours ago | parent | next [-]

I know that Solaris (or at least, ZFS) has VERIFY and ASSERT macros where the ASSERT macros are compiled out in production builds. Is that the kind of thing you're referring to?

You can aslo mark certain codepaths as unreachable to hint to the compiler that it can make certain optimisations (e.g., "this argument is never negative"), but if you aren't validating that the assumption is correct I wouldn't call that an assertion -- though a plain reading of your comment would imply you would still call this an "assertion"? AFAIK, no language calls this construct "assert".

This is probably one of those "depends on where you first learned it" bits of nomenclature, but to me the distinction here is between debug assertions (compiled out in production code) and assertions (always run).

▲

nothrabannosir 14 hours ago | parent | prev [-]

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?

▲

bluGill an hour ago | parent [-]

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)

	▲	empath75 17 minutes ago \| parent [-]
		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.

▲

kg 14 hours ago | parent | prev [-]

> 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.

▲

voxl 11 hours ago | parent [-]

You already have hardware level bit flip verification, you don't need to recheck the list

	▲	tsimionescu 9 hours ago \| parent \| next [-]
		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.
	▲	comex 11 hours ago \| parent \| prev [-]
		Only if you have ECC RAM, and even then it’s not perfect.