Another idiom I wish were gone from phobos/druntime

[via Digitalmars-d]

On Thursday, 5 February 2015 at 09:43:53 UTC, Jonathan M Davis 
wrote:
> There is no such difference in the current implementation. 
> assertions inside
> of in and out blocks are no different from assertions inside of 
> the
> functions themselves with regards to when they are compiled in 
> or not.

But that is a compiler issue, and not a general issue with 
interface contracts for components.

What is desirable is to have "asserts with semantics attached to 
them" done in a way that works with how you do formal program 
verification. I also would like to see loop invariants getting a 
special treatment.

> pass. Regardless,
> if you have
>
> auto foo(T t)
> in
> {
>     assert(something about t);
> }
> body
> {
>     ...
> }
>
> it's _identical_ to
>
> auto foo(T t)
> {
>     assert(something about t);
>     ...
> }

Yes and just having an alias "precondition" for "assert" would go 
a long way in that case. And if the compiler recognize it, it 
could also do the magic for inheritance.


> with regards to semantics. Ideally, what's in the in block 
> would be compiled
> in if the caller is compiled with assertions enabled with no 
> regard to
> whether the library with foo in it was compiled with assertions 
> enabled or
> not, but that's not how it works. And because D allows for 
> function
> prototypes where the implementation is hidden, it's not at all 
> obvious how
> it would even be possible for anything in an in our out block 
> could be
> compiled in or not based on the caller rather than the function 
> itself.

I actually think that interface contracts (and ideally unit 
tests) should be part of a specification language that is shared 
across implementation languages. Then the implementation language 
has to provide mechanisms to make it possible to test that the 
transitions between components abide interface contracts.

The ideal build system would allow you to have one specification 
with pre/post conditions between modules and then let the build 
system link together "LLVM IRish object code" with checks between 
modules injected duing whole program optimized "linking".

That way you could build large systems that are more robust using 
code from C, C++, Ada, Fortran, Rust, D... governed by one 
unified specification. And a combination of proof verification 
and an optimizing linker could elide pre/post-condition tests 
that are redundant, either before a formal proof exists that only 
needs to be verified or because the condition is trivially 
satisifie, e.g.:

----

func(int i){
   precondition(i>0);
   ...
}

----
func(3);
-----