"Artur Skawina via Digitalmars-d"  wrote in message news:mailman.217.1406713015.16021.digitalmars-d@puremagic.com...

> `assert` is for *verifying* assumptions. It must not allow them
> to leak/escape. Otherwise a single not-100%-correct assert could
> defeat critical runtime checks.

All you're saying is you want them to have different names, not that it can't work the way Walter and I have described.  If your assertions are invalid and you're compiling with -release, the compiler is free to generate invalid code.  -release is dangerous.  -release is telling the compiler that the code you wrote is correct,  and it can rely on it to be correct. 

"Ola Fosheim Grøstad" " wrote in message news:ilqxnvyqwfmcasxnbjko@forum.dlang.org...

> Here is a link to the original paper where C.A.R. Hoare introduces assertions. Yes "assert()" in C is the same. The D spec claims to provide C-style assertions. That means it should abide to what is described in this paper:
>
> http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf
>
> If not, call it something else.

So you'll be happy if we call them D-style assertions? 

On Wednesday, 30 July 2014 at 12:11:31 UTC, Daniel Murphy wrote:
> So you'll be happy if we call them D-style assertions?

Program verification has been at the core of CS for over 40 years. This is bachelor grade stuff. If you keep inventing your own semantics for well-established terminology then nobody will take D seriously.

For instance, if assert(false) is proven reachable then it means either:

1. the specification is inconsistent/contradictory (thus wrong)
2. the program has been proved incorrect

The compiler should then refuse to generate code. If it is not proven reachable then emitting HALT might be ok.

Basically D ought to allow a verifier to work on a D program, then only emit runtime checks for asserts it cannot handle. And also allow them to trigger as early as possible.

On Wednesday, 30 July 2014 at 09:12:56 UTC, bearophile wrote:
> And assume() and assert() are two different things, used for different purposes. Do not give the same name to two so different features, if you want to keep a language sane.

Exactly. If you want to establish that the provided input is never zero and that the program doesn't need to be correct in that case, you do this:

assume(input!=0);

If you want to specify that the input should be prevented from being zero, you do this:

if(input!=0){
  assert(input!=0);
}

"Ola Fosheim Grøstad" " wrote in message news:umhhokwldfouodjhvooh@forum.dlang.org...

> Program verification has been at the core of CS for over 40 years. This is bachelor grade stuff. If you keep inventing your own semantics for well-established terminology then nobody will take D seriously.

It sure seems easy to make D not be taken seriously.  Every day somebody's making this claim about something.

> For instance, if assert(false) is proven reachable then it means either:
>
> 1. the specification is inconsistent/contradictory (thus wrong)
> 2. the program has been proved incorrect
>
> The compiler should then refuse to generate code. If it is not proven reachable then emitting HALT might be ok.

You say this as if it's a law of physics.  One of the great things about working on D is that we get to assign the semantics that we decide are most useful, and don't have to follow what other people have done.

A good example is D's purity.  It doesn't match traditional definitions of purity, but it's useful.  I'm sure that's another reason not to take D seriously.

> Basically D ought to allow a verifier to work on a D program, then only emit runtime checks for asserts it cannot handle. And also allow them to trigger as early as possible.

You're just saying it should work the way you think it should work.  The fact that other people have defined it that way before does not outweigh the value of defining assert the way I've described IMO.  I don't think the safety concerns are warranted either, due to the existing optimizer precedent.

Any verifier for D would have to understand the semantics of D's assert.  If the verifier assumes asserts are always replaced with a runtime check, then it will be fine as long as you don't compile with -release. 

On Tuesday, 29 July 2014 at 19:35:31 UTC, Walter Bright wrote:
> To have an assert despite -release, you can do things like:
>
>    assert(exp);  =>  if (!exp) assert(0);
>
> I generally leave asserts in for released code in my projects.

You honestly don't smell a problem here? There is a default behavior dmd uses and you (compiler author!) disable it because non-default one seems more practical. If this does not indicate something is wrong with the system I don't now what does.

> You can see this in dmd which often exhibits a fault as a tripped assert.

Exactly. And same is for our Sociomantic projects - those never get compiled with -release because programs have bugs and you want to be able to detect bugs instead of corrupting the service.

asserts indicate bug in program logic but removing them in release builds means letting those bugs lose. In practice I can't imagine a situation where one can afford such risk, not even with 100% test coverage (because code paths that trigger assertions are not covered in a working program)

> It's a serious, serious mistake to use asserts for user input validation. If passing raw user input to a library function, unless that function is specifically documented to validate it, you've made a big mistake.

I know it all well and it doesn't help in practice even tiny bit. It is not something as naive as just calling the function with user input. All such cases are programming bugs that do not get caught by tests but trigger upon user input code paths. Bugs that will get unnoticed if default -release is used.

>> It feels like for contracts to really work some good implementation of red-green
>> code zones is necessarily, to be able to distinguish user input call paths from
>> internal ones during compilation time.
>
> That's not what contracts are for (beating a dead horse).
>
> Joel Spolsky made a suggestion I like - have raw user input be of a different type than validated input. That way, functions are clearly and checkably red-green zoned.

Ironically it is the very same thing I have suggested in quoted part but you call it wrong :) Thew way it interacts with contracts is that it becomes possible to define validated program sub-system known at compile-time which has much better chance to be tested good enough to afford omitting assertions and contracts.

"Andrei Alexandrescu"  wrote in message news:lr8tcf$l1t$1@digitalmars.com...

> Fancier: exp || assert(0) is still an expression.

Fancier is not always better. 

On Wednesday, 30 July 2014 at 13:14:11 UTC, Daniel Murphy wrote:
>> For instance, if assert(false) is proven reachable then it means either:
>>
>> 1. the specification is inconsistent/contradictory (thus wrong)
>> 2. the program has been proved incorrect
>>
>> The compiler should then refuse to generate code. If it is not proven reachable then emitting HALT might be ok.
>
> You say this as if it's a law of physics.  One of the great things about working on D is that we get to assign the semantics that we decide are most useful, and don't have to follow what other people have done.

It follows the law of logic:

http://en.wikipedia.org/wiki/Hoare_logic
http://en.wikipedia.org/wiki/Propositional_calculus

> Any verifier for D would have to understand the semantics of D's assert.

If D gets this it will be a general verifier adapted to D. That follows the rules of established sound logic developed over the past 2300 years.

All asserts should be established as either true or unknown. Assert(false) is weird. It is basically saying that true==false and asks you to prove that over a statement/loop that may or may not terminate.

http://coq.inria.fr/distrib/8.2/contribs/HoareTut.exgcd.html

«Basic Hoare logic is not well-suited for reasoning about non-terminating programs. In total correctness, postconditions of non-terminating programs are not provable. In partial correctness, a non-terminating program satisfies any (unsatisfiable) postcondition.»

"Walter Bright"  wrote in message news:lr8t23$kof$1@digitalmars.com...

> To have an assert despite -release, you can do things like:
>
>     assert(exp);  =>  if (!exp) assert(0);

dmd does currently implement it that way, but the spec explicitly says the compiler may assume it is unreachable and optimize based on that.

'halt' is what you should be calling if you want to guarantee a halt in -release mode. 

"Ola Fosheim Grøstad" " wrote in message news:lzrtpkfytndikacweici@forum.dlang.org...

> It follows the law of logic:
>
> http://en.wikipedia.org/wiki/Hoare_logic
> http://en.wikipedia.org/wiki/Propositional_calculus

You're missing the point - we don't have to follow those definitions.  Maybe we should - but the fact that those systems are defined that way doesn't intrinsically mean we have to define asserts behaviour that way.

> > Any verifier for D would have to understand the semantics of D's assert.
>
> If D gets this it will be a general verifier adapted to D. That follows the rules of established sound logic developed over the past 2300 years.

Yes, and the adaption will have to take into account D's semantics.  This doesn't mean D can't differ from other established definitions.

> All asserts should be established as either true or unknown. Assert(false) is weird. It is basically saying that true==false and asks you to prove that over a statement/loop that may or may not terminate.

assert(false) is saying that the condition will never be met, and that branch of execution is impossible in a correct program.  (although it is often abused to mean 'unimplemented')