>An “invariant” is a function of the process state whose value remains constant (hence “invariant”) in spite of changes to the process state. Perhaps you meant “precondition” or “postcondition”?
No, I meant invariant. An invariant is something that is supposed to hold true, not just things that are guaranteed to hold true (e.g. a constant that can't ever change anyway). That's why the need for assertions to check that invariants hold.
From Wikipedia:
"In computer science, an invariant is a condition that can be relied upon to be true during execution of a program, or during some portion of it. It is a logical assertion that is held to always be true during a certain phase of execution. (...) Programmers often use assertions in their code to make invariants explicit."
Preconditions and postconditions are similar in concept, but are supposed/wanted to hold true before (pre) or after (post) a method runs.
>I absolutely don't need asserts. An assert merely describes what you want, but that's useless to me, unless you establish a relation between what you want and what your program actually does - with proof.
Well, asserts weren't created specifically for you. Feel free not to use them.
They are useful to me, and assuming from their widespread use, others, even if they don't formally prove the program does 100% that it needs to (which nobody expected them to anyway).
Until we all program in Coq or similar, they will be useful for all kinds of checks. A correct program is a spectrum, not a binary option.
>Of course. Assertions are expected to always be true.
No, they are also expected to be false -- that's why we add assertion statements to check whether our assertions hold. But we're splitting hairs twice or three times here.
> That's why the need for assertions to check that invariants hold.
No, you need proof.
> Until we all program in Coq or similar
So you're saying humans are fundamentally incapable of establishing the logical validity of what they assert by themselves? This contradicts historical evidence that people have done this for well over 2 millennia, using various methods and tools.
> A correct program is a spectrum, not a binary option.
Some errors might be easier to fix or have less disastrous consequences than others, but a correct program is one that has no errors, so I don't see where the spectrum is.
>That's why the need for assertions to check that invariants hold.
>No, you need proof.
You might need proof, but it doesn't mean you'll get it. In most languages in common use (e.g. not Coq and co) and for any larger than trivial program "proof" is impossible.
So, we'll continue to need all the tools we can realistically use, including assertions, unit tests and others.
>So you're saying humans are fundamentally incapable of establishing the logical validity of what they assert by themselves? This contradicts historical evidence that people have done this for well over 2 millennia, using various methods and tools.
This particular question is not even wrong in the context of the discussion. I don't usually throw around the term "troll", but you're either trolling or being alternatively naive on principle / too pedantic.
I any case, whether people are "capable of establishing the logical validity of what they assert by themselves" for trivial things or for narrow domains, the absolutely have not been able to manually do it, or do it fast enough to be practical, for software programs, especially any non trivial one. Even the best programmers introduce bugs and have behavior in their program that they didn't expect.
Which is also why even the best programmers use assertions. It's not some obscure feature relegated to newbies or bad programmers. It's a standard practice, even in the most demanding and hardcore programming environments, from the Linux kernel (which uses the BUG_ON assertion macro) to NASA rocket code.
Or I could turn "troll mode" on an answer on the same vein as the question: if "people have done this for well over 2 millennia, using various methods and tools" then they haven't been doing it "by themselves" any more so than when using assertions (which is also one of such "tools").
And of course, I haven't anywhere stated that "humans are fundamentally incapable of establishing the logical validity of what they assert by themselves".
The gist of my comment would be merely that humans are bad at establishing the logical validity of their computer programs by themselves -- for which there is ample "historical evidence".
>Some errors might be easier to fix or have less disastrous consequences than others, but a correct program is one that has no errors, so I don't see where the spectrum is.
The spectrum is obviously in that correctness is not black and white, and all non trivial programs have bugs in practice. Those programs with few and far between bugs are more correct than others.
No, I meant invariant. An invariant is something that is supposed to hold true, not just things that are guaranteed to hold true (e.g. a constant that can't ever change anyway). That's why the need for assertions to check that invariants hold.
From Wikipedia:
"In computer science, an invariant is a condition that can be relied upon to be true during execution of a program, or during some portion of it. It is a logical assertion that is held to always be true during a certain phase of execution. (...) Programmers often use assertions in their code to make invariants explicit."
Preconditions and postconditions are similar in concept, but are supposed/wanted to hold true before (pre) or after (post) a method runs.
>I absolutely don't need asserts. An assert merely describes what you want, but that's useless to me, unless you establish a relation between what you want and what your program actually does - with proof.
Well, asserts weren't created specifically for you. Feel free not to use them.
They are useful to me, and assuming from their widespread use, others, even if they don't formally prove the program does 100% that it needs to (which nobody expected them to anyway).
Until we all program in Coq or similar, they will be useful for all kinds of checks. A correct program is a spectrum, not a binary option.
>Of course. Assertions are expected to always be true.
No, they are also expected to be false -- that's why we add assertion statements to check whether our assertions hold. But we're splitting hairs twice or three times here.