https://issues.dlang.org/show_bug.cgi?id=23996

elpenguino+D@gmail.com changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |elpenguino+D@gmail.com

--- Comment #1 from elpenguino+D@gmail.com ---
I think assert(expr) could provide this functionality. Maybe with a -checkaction=assume switch? It would also work for contracts, invariants, etc then, while also making it trivial to test the assumptions.

--

https://issues.dlang.org/show_bug.cgi?id=23996

timon.gehr@gmx.ch changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |timon.gehr@gmx.ch

--- Comment #2 from timon.gehr@gmx.ch ---
`assert(expr)` does not fit the bill because it is `@safe`. -checkaction=assume
can still happen in principle (as a similarly unsafe flag like -noboundscheck),
but it's orthogonal.

--

https://issues.dlang.org/show_bug.cgi?id=23996

mhh <maxhaton@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |maxhaton@gmail.com

--- Comment #3 from mhh <maxhaton@gmail.com> ---
Should be an intrinsic or a UDA, pragmas are an anti-pattern.

--

https://issues.dlang.org/show_bug.cgi?id=23996

--- Comment #4 from Bolpat <qs.il.paperinik@gmail.com> ---
(In reply to mhh from comment #3)
> Should be an intrinsic or a UDA, pragmas are an anti-pattern.

Could you elaborate how it should look like?
I don't see how a UDA would work syntactically.
An intrinsic must be protected by `version` to ensure the compiler supports it.
How is a pragma an anti-pattern? Inline is a pragma.

In C++, it was an intrinsic, but every compiler had a different one, so in C++23, it became part of the standard so that it's not an intrinsic anymore.

--

https://issues.dlang.org/show_bug.cgi?id=23996

--- Comment #5 from Bolpat <qs.il.paperinik@gmail.com> ---
(In reply to elpenguino+D from comment #1)
> I think assert(expr) could provide this functionality. Maybe with a -checkaction=assume switch? It would also work for contracts, invariants, etc then, while also making it trivial to test the assumptions.

I’d say this is really bad design. An assertion and an assumption mean totally different things. With a compiler flag, you control all of them at once.

Just for an example, an assumption can be used to inform the compiler about a
truth that its optimization routines can make use of and that its optimization
routines could not figure out themselves.
An assert might be used to validate function input, e.g. `isPrime(int x)` might
`assert(x > 0)`.

--

https://issues.dlang.org/show_bug.cgi?id=23996

--- Comment #6 from elpenguino+D@gmail.com ---
(In reply to Bolpat from comment #5)
> (In reply to elpenguino+D from comment #1)
> > I think assert(expr) could provide this functionality. Maybe with a -checkaction=assume switch? It would also work for contracts, invariants, etc then, while also making it trivial to test the assumptions.
> 
> I’d say this is really bad design. An assertion and an assumption mean totally different things. With a compiler flag, you control all of them at once.
> 
> Just for an example, an assumption can be used to inform the compiler about
> a truth that its optimization routines can make use of and that its
> optimization routines could not figure out themselves.
> An assert might be used to validate function input, e.g. `isPrime(int x)`
> might `assert(x > 0)`.

An assertion is just an enforced assumption. They both mean the same thing.

assert():
- code following is optimized with the assumption that the condition is true
- undefined behaviour if condition is false

pragma(assume):
- code following is optimized with the assumption that the condition is true
- undefined behaviour if condition is false

It is legal for assert() to influence the optimizer without actively checking the condition, and this proposal would also allow a compiler to actively check and enforce the condition in pragma(assume) - it is undefined behaviour, and it might be useful to prove your assumptions while debugging.

Enabling assertions to be treated as unchecked assumptions additionally allows for invariants and contracts to influence optimizations, though current compilers don't appear to be capable of optimizing invariants...

--

https://issues.dlang.org/show_bug.cgi?id=23996

--- Comment #7 from timon.gehr@gmx.ch ---
(In reply to elpenguino+D from comment #6)
> (In reply to Bolpat from comment #5)
> > (In reply to elpenguino+D from comment #1)
> ...
> An assertion is just an enforced assumption. They both mean the same thing.
> ...

They are dual. An assertion is a proof obligation, an assumption is an axiom.

It's more obvious in a verifier. Standard definitions in Hoare logic:

{ P ∧ Q } assert(P) { Q }
{ Q } assume(P) { P ∧ Q }

In D, `assert` is `@safe`, `assume` has to be `@system`. You can't do hard optimizations based on unchecked assumptions (in particular in `@safe` code) while following the D specification, any flag that does so deviates from the specification of `@safe`. This is why this enhancement is important, it enables actually giving `@trusted` optimization hints in a sound manner.

--