Void safety clashes with DbC (it forces us to indulge in defensive programming). What is more, it doesn't give you void safety!
Here is an example of a class that forces us to use defensive programming (I actually used a check statement, rather than the proper defensive style of an object test with raising an exception in the else branch - see `fromJust'):
class MAYBE [G]
create
make,
make_nothing
feature {NONE} -- Implementation
make_nothing is
-- Create as object absent.
do
ensure
no_object_present: is_nothing
end
make (a_object: !G) is
-- Create with object.
do
object := a_object
ensure
object_present: is_just
object_set: object = a_object
end
feature -- Access
from_just: !G is
-- Contained object
require
object_present: is_just
local
l_object: ?G
do
l_object := object
check
l_object_not_void: l_object /= Void
-- From precondition
end
Result := l_object
end
feature -- Status report
is_nothing: BOOLEAN is
-- Is an object absent?
do
Result := (object = Void)
ensure
definition: Result = (object = Void)
end
is_just: BOOLEAN is
-- Is an object present?
do
Result := not is_nothing
ensure
definition: Result = not is_nothing
object_not_void: Result implies object /= Void
end
feature {NONE} -- Implementation
object: ?G
-- Possible contained object
end
Thanks to the check statement, the class compiles. But it is horrible to have to write code that assumes the precondition might be wrong. This is a direct contradiction of the DbC style.
Finally, if we deliberately violate the precondition, the program still compiles. The so-called Void safety is buying us nothing. Here is a root class:
class TEST
create
execute
feature -- Test
execute is
-- Execute test.
local
l_maybe: MAYBE [STRING]
l_string: !STRING
do
create l_maybe.make_nothing
l_string := l_maybe.from_just
print (l_string.out)
end
end
no gains
It seems that your post is missing the part where you talk about the call on void target that you had (I assume that you had one since you assert so forcefully that the new mechanisms of Eiffel does not provide void-safety).
In case you didn't know, in general, the problem of inferring from your precondition the fact that `object' is attached is an undecidable problem. There is a set of simple rules to rule out a great deal of calls on targets. For the rest, I agree, it can produce some ugly code but we should think that this is the last word on void-safety; there's still many heuristics that could be exploited to improve the situation tremendously.
I have personally been involved in the conversion of a non-trivial amount of Eiffel code to void-safety and, although it drove home the point that the mechanism could be improved a great lot, it also allowed me to find subtle but important design flaws in a code base I had not been working with for a long time.
I think it this respect, nuancing your statement on the whole endeavor would be much more constructive. As far as I'm concerned, there is definitely a gain.
Regards,
Simon
No, I didn't miss out anything.
There is no safety gained by turning on void safety checking here. Merely a burying of the bug (when finalized), and obscuring the code. Why do you say that the inference is undecidable? The reasoning chain looks very short and straight-forward to me.
Colin Adams
Oh yes, I missed out the .out.
The last line should read print (l_string.out) Colin Adams
I've fixed your entry.
Void-safety guarantees no void target calls
Colin, this is an interesting case. I looked at 'from_just' and recognised that the defensive 'check' statement is needed only because you wrote the precondition in terms of the 'is_just' query. If the precondition had asserted directly that 'object /= Void', then this would have been a certified attachment pattern (CAP), which would have been sufficient to tip the compiler off that 'object' is attached. No check statement needed. So why is your example interesting? Because in a case like this, where the visibility of 'object' is more restricted than the visibility of the routine, you must write the precondition in terms of a sufficiently visible query such as 'is_just'; and therefore, the CAP is not available. As a consequence, the nasty defensive-programming hack seems unavoidable.
In your introduction, you claim that void safety "forces us to indulge in defensive programming". Is such a broad, blanket statement justified by the single example of 'from_just'? Although similar real-world functions exist, such cases are very rare, aren't they? I would agree with your claim if it was qualified: void safety "forces us to indulge in defensive programming in rare corner cases".
Your second claim, however, that void safety "doesn't give you void safety", is completely unsubstantiated. You seem to base it on the observation that, "if we deliberately violate the precondition, the program still compiles." Sorry, but the claim does not follow from this observation. Precondition violations are checked at run-time, as you well know; always have been, and still are. Void-safety hasn't changed that fact. The whole point of void-safety is to guarantee not that the program will never crash, but rather to guarantee that it will never crash with a void target call. Void safety does not equip Eiffel compilers with the ability to prove DbC assertions statically. When you call 'l_maybe.from_just', the program crashes: not from a void target call, but from a precondition violation.
Nice try, but if you're hoping to knock void safety off its exalted pedestal, you'll have to come up with a better argument than saying that it doesn't achieve something it wasn't even attempting!
Not rare at all!
Firstly, /= Void in a precondition is not a CAP - I just confirmed that by changing the code - now it won't compile.
Secondly, preconditions with /= Void are widespread - hardly a rare corner case - so my assertion is quite justified. Thirdly - preconditions are not checked at runtime unless you have monitoring turned on - this is not normal for finalized systems. Fourthly - the program crashes with a void-target call (when the missing .out is added back in).
And what pedestal? It has never been on one. It is unusable, unless you abandon DbC.
Colin Adams
Void safety is
You're right on the first point, Colin, at least insofar as it doesn't compile in EiffelStudio 6.4. I just tried it too - it doesn't compile. I recall a discussion on the Eiffel Software mailing list a few months ago, however, that indicated that this is a CAP in the Eiffel standard. Unless my memory is failing me (highly possible) this is a limitation of the current EiffelStudio implementation, not of void safety per se.
On your second point, yes, preconditions like this are widespread, but if they are indeed a CAP then the situation you've shown is, I suspect, a corner case. I look forward to finding out whether I'm wrong about this ;-)
Skipping now to your fourth point, I just copied your classes into EiffelStudio and ran it. It fails on the precondition, not on a void call. It never reaches the void call. Void safety is, and here's the proof, from your own code:
object_present: Precondition violated. (PRECONDITION_VIOLATION) ------------------------------------------------------------------------------- Class / Object Routine Nature of exception Effect ------------------------------------------------------------------------------- MAYBE from_just @1 object_present: <0000000001B00444> Precondition violated. Fail ------------------------------------------------------------------------------- TEST make @2 <0000000001B00414> Routine failure. Fail ------------------------------------------------------------------------------- TEST root's creation <0000000001B00414> Routine failure. Exit ------------------------------------------------------------------------------- No void target call there. Just a good old fashioned precondition failure. Stepping back to your third point, ok, if you turn off assertion checking then of course the program will not check the precondition and, yes, it will crash a bit later with the void call. I can't see the relevance to your argument. If you turn off assertion checking then yes, of course you'll get weirdo crashes. This has always been the case with DbC. Void safety, like everything else in Eiffel, is designed to work in conjunction with the contracts. I think the title of your article is wrong, Colin. Instead of "Void safety isn't", you should have called it "DbC isn't", because you've actually just presented the old argument that DbC is worthless if the assertions are not checked statically and you have to turn them off to get decent performance in a real system. And about the pedestal: void safety sure is on a pedestal from where I stand, on two counts. First because it promises to fulfil a long-held wish of mine to eliminate the most common cause of program crashes. (I do a lot of C# programming these days, and I am plagued daily by the dreaded NullReferenceException.) Second because I haven't converted our Eiffel code yet (partly due to lack of time, but mainly because it would probably be pointless to do so until Gobo is void-safe), so void safety is sitting up there, all shiny-looking, but I can't touch it yet. Finally, that last little throw-away line of yours, "It is unusable, unless you abandon DbC." Clearly wrong, according to these links: http://dev.eiffel.com/Void-Safe_EiffelStudio_Status http://dev.eiffel.com/Void-Safe_Library_Status Keep trying, Colin, the debate is interesting ;-)
Where does anyone claim (prior to you on this thread) that void-safety only works if assertion-monitoring is turned off? On the contrary, the compiler is supposed to keep check assertions enabled if it can't prove them to be true (clearly 6.4 doesn't). Colin Adams
Keeping check assertions when assertions are off?
I'm not sure what you mean, Colin. If assertions are switched off, then ... they are switched off, aren't they?
My point is simply that the compiler approved the code as "void safe" on the basis of the assumptions that you have stated in your assertions. If assertions are switched off, and one of those assumptions turns out to be false, then your program is likely to crash. This is DbC as we have always known it. There's nothing new about this.
Are you suggesting that the compiler should keep some of the assertions, despite having been told to discard them?
That's what ECMA says.
Anyway, it isn't DbC as we have always known it. I do not have to repeat my postconditions with check statements now. To compile in void-safe mode, I do. This is a non-starter. Colin Adams
Peter, Colin is right in that ECMA will preserve contracts in a compilation where assertions are discarded, but are required for proof of Void-Safety. The check statement inl_object ' will indeed be attached. This would require deep code analysis and will likely detriment compiler performance. However, when executing, a call on a Void target will never happen because a check violation will occur.
<e>from_just</e>' will be preserved because the compiler cannot statically prove (yet)It's important to separate DbC from Void-Safety. To date we've been use DbC to prevent calls on Void targets and I think it's easy to lump them into the same mechanism. Contracts are runtime checks and Void-Safety are static checks. The line also becomes blurred between them because we can use certain contract clauses as a CAP. However a precondition is not safe to use as a Void-Safety check. In a multithreaded system, a precondition can be checked, another thread awoken (setting `object ' to Void) and execution continues as normal. A void target call occurs as a result, ergo - precondition are not safe of CAPs.
One thing we introduced, and are yet to form an official syntax for yet, is stable attributes. Although a defensive stance is still taken it avoids issues with multithreading cases prevent the compiler from proving a target is attached, as once attached it can never become detached:
Like the previous code, thecheck will remain functional even when discarding assertions.
My final thing I want to talk about is the Void-Safety mechanism itself and it's "pedestal". I've been using the attachment mechanism from day one. It was a rocky start as we were still trying to figure things out and certain CAPs had not been implemented or realized yet, but it wasn't publicly release either. Things got much better in 6.4 and are fantastic in 6.5. Yes, yes, converting existing code can be a royal PITA but Void-Safety introduces a shift in the way we think about our code. As a result some of the converted code isn't looking that way we want it too because of the assumptions made, but on the contrary, some converted code took no changes at all. All new developments I do are using attached-by-default and fully Void-Safe and I can tell you without a doubt, it's a life changing language feature! If it's not on a pedestal then it should be! I also do a lot of Objective-C development and it literally scares me at times, as I simply cannot prove an entity wont give me `
nil'. The same is true for C#.We can argue that using DbC that we've long since seen a feature call made on a Void target but the reality is, that it's not a validation mechanism of the compiler that make this happened but a more careful thought process. Writing a precondition enforce a thought pattern, which is why it's good practice to always write them before any code, that or a precondition violation at runtime. It is true that it has been a long time since I have seen a feature called on a Void target, but I've seen plenty of precondition violation that check attachment state. The Void-Safety mechanism takes it one step further and force that way of thinking and tries to guarantee you'll never the code never flows to an execution path, resulting in a Void target call. Since using Void-Safety, it's been very, very rare to see any condition that results in a Void target call. The only exception is when making an assumption and fooling the compiler - a hack is a hack and you get what you deserve!
CAPs
"However a precondition is not safe to use as a Void-Safety check. In a multithreaded system, a precondition can be checked, another thread awoken (setting `object' to Void) and execution continues as normal. A void target call occurs as a result, ergo - precondition are not safe of CAPs."
It seems acceptable that the occurence of
in the precondition be not taken as a garantee that the attribute `object' is attached but changing it slightly can change the situation around completely. Indeed, replacing the equality test with
will ensure that
obj' is attached during the execution of the routine. Accepting the use ofobj' in the body of the routine would be in direct line with avoiding the defensive style that Colin and Eric are complaining about and, frankly, I agree with them in that I would rather avoid piling up defensive style on top of DbC (and please do not infer that I would prefer get rid of DbC first!). However, I don't equate attached types with defensive programming.Simon
Static type-checking of contracts is necessary
I don't equate attached types with defensive programming either. Nor for that matter, do I equate void-safety with defensive programming - just the type of void safety advocated by ECMA.
Void safety and DbC can go hand-in-hand. But checking void-safety purely locally (e.g. saying that because a routine is only void-safe if the precondition is fulfilled - and therefore we will reject this class as not void-safe) is not on - you have to do static type checking (of the contracts) at the system level. This is the approach taken by Haskell/ESC, which adds contracts to an inherently void-safe language (since Haskell does not have Voids).
See http://www.cl.cam.ac.uk/~nx200/
Colin Adams
I saw your comment on this further down, it's a good idea and we have looked at it. Having a precondition that does this is fine until you start redefining that feature. The local 'obj ' becomes invisible to the redefined feature and can confuse readers as to where 'obj ' originates from. You could add a require else however this introduces duplicate code and potential bugs in the future (when the base preconditions change). Things get even more confusing when selecting and redefining a feature on a branch when using multiple inheritance. There was talk about restricting this type of check to the enclosing contact clause only, which would be very useful.
Gobo not void-safe
The reason why Gobo is still not officially available in void-safe mode is exactly for the same concerns as Colin's. It introduces too many code duplication and defensive programming to my taste. And no, they are not corner cases. Perhaps the reason why no one else seems to have the same feeling is that Gobo is using DbC in a deeper way. For me there is no pedestal about void-safety. I'm glad to hear that it allows some people to find and fix bugs. But my personal experience shows that in addition to code duplication and defensive programming, void-safety is in many cases nothing else than replacing call-on-void-target exceptions by other kinds of exceptions. I can understand that call-on-void-target exceptions are something that people get more often than they would like. But thanks to a good use of DbC (I mean Design by Contracts, not Debug by Contracts), I quite successfully managed to stay away from this kind of exceptions so far. As a consequence you can understand that it is quite hard to swallow the fact that now I have to duplicate code and use defensive programming in order to make the compiler happy for an goal that is not entirely fulfilled. Indeed the promise to catch call-on-void-target at compile time is not that appealing if in many cases we have to replace this kind of exceptions by other kinds of exceptions. Of course people experience (or non-experience :-) ) may differ.
Puzzled
Eric, I'm curious about your experience that void safety often just trades void target calls with other exceptions, so I have a couple of questions.
1. What exceptions are these?
2. Does this occur any more frequently than in traditional Eiffel, where (as Paul mentioned) we rarely saw void target calls either because we usually got a different exception first, namely, a failed /= Void assertion.
call-on-void-targets replaced by other exceptions
1.
First, we have to agree that void-safety forces us to duplicate code and use defensive programming in order to make the compiler happy. For me, using the programming pattern shown by Zoran with the feature always returning an attached object and using a default value in case it does not make sense is most of the time not acceptable: there is a risk to get data corruption far away from the source of the problem.
So, what do we do in order to make the compiler happy? We can use the check-instruction. In that case, assuming that you used to get a call-on-void-target exception, now you will get a check-violation exception. OK, we got rid of the call-on-void-target exception, but we still have an exception. Its name is just different. Now instead of the check-instruction we can use an object-test. But what do you do in the else-branch of the if-instruction? Do you just put your head in the sand and ignore the problem. Or do you raise a (developer) exception?
2.
If a program is correct, according to Eiffel's spirit, no exception should occur. So that does not change. Void-safety is about getting rid of call-on-void-target exceptions, not about getting rid of assertion violations (although this would something that would really deserve a pedestal). So if you don't get call-on-void-target exceptions that often, that will not change. If you were getting precondition violations of the form "/= Void", there are 3 cases. Either you will be able to rewrite your code in such a way that this assertions will not exist anymore without introducing defensive programming. People in this forum claim they managed to do so. More often than I would like I'm not that lucky. Or you have to rely on a programming pattern using a dummy value to guarantee that the return value is always attached. Then who knows whether you will get data corruption or not. Or finally will get other kinds of exceptions.
If this problem was converted to a polymorphism example, I don't think we'd be making the same arguments; attachedness is like extra type information.
Maybe there's an issue with the `check var /= Void end' pattern but I don't see how this makes the entire void-safe system bad.
If this compiled I think everyone would argue, why is this being done? This is working around the type system.
This is as an undesirable pattern anyway
I haven't used void safety at all (I'm still developing on 5.7!), but I don't really see why you would use this design in a void safe world. The problem stems from an attempt to give clients attached semantics for an object that isn't really attached. Without void safety this pattern makes sense. The precondition alerts clients that the object may by void and "prevents" (via the relatively weak run time precondition check) a call on the void object. With void safety it would make more sense to expose the unattached object directly. Now you have stronger compile time protection against a call on the void object. This doesn't place any additional burden on the client. It just changes the syntax the client uses to access {MAYBE}.object
becomes (something like)
This also allows you to remove a bunch of code in MAYBE.
Rare corner cases
I think your point is exactly right, Neal. I started to write pretty much the same in my initial reply to Colin's post; I think I wrote that Colin's example was "contrived", for exactly the reasons you've described. But then I deleted it all to give Colin the benefit of the doubt, because I can see that there may be rare occasions when you would want to write a function like 'from_just'. Like I said in my original reply: rare corner cases.
My example wasn't contrived at all, because when I wrote the class, I wasn't thinking about void-safety - it was for a very different purpose.
But as I wasn't intending to check the class in, it occurred to me that I could check out support for void-safety in 6.4. I had never touched void-safety before, because I knew the class wasn't there. So I turned on full checking in the ecf, and found it wouldn't compile unless I added the check statement.
So I have encountered a 100% failure rate with void-safety. Of course the sample will not be representative, but this is typical DbC style, so I would expect many more. In any case, we won't be going to void-safety, my boss said don't even think about it.
Colin Adams
failure rate
As you said, your experiment is of really small scale and I don't think it would warrant such an automatic rejection. For one thing, one the complains that you make basically boil down to: "Aw man, I can't do the things exactly the way I use to and have the compiler find the bugs for me". It seems quite unrealistic to expect an improvement without change.
In this case, the compiler needs a clear hint that it can rely on
object' being attached. Ifobject' was exported, we could replace the precondition byand expect it to do the trick. Unfortunately, using object test locals declared inside preconditions is not supported yet. In any case, it wouldn't exactly do the trick since object is not exported.
The kind of rule that would make your example satisfactory (if I understood your expectations properly) is one that would make usage of information present verbatim in the postcondition of `is_just' and allow us to repeat it as an object test with a local in the precondition. This is not independent from the first rule; we need to be able to use object test locals declared inside preconditions.
I don't think we need to support a very fancy class of postconditions for this to be very useful. For example, if we consider propositions where basic propositions are boolean entities or object test on entities (as opposed to arbitrary expressions), we could have a nice horn clause in the postcondition and extract information from it and use it in a precondition.
which we could use as follows:
The part attached object as obj is really a hint to the compiler and needs not appear in flat view. However, it needs to be there to make sure the object test local does not clash with other locally available entities.
The moral of the story is that attached types is still a young mechanism and we have to admit that it can't cover every possible case the mind can conjure since it would not be a solvable problem. Therefore, we have to be patient and try and see how it can improve our programming style when it's possible and how we can reduce the inconvenience. I have the firm conviction that it can get better and that, when it gets ready, it will be of tremendous value to eliminate bugs and design flaws before they even manifest themselves.
Cheers!
Simon
Example uses obsolete constructs
The notation '!' and '?' is obsolete now. Also, this was tried in a mode where the compiler ignores almost completely '!' and '?' (depending on which version of the compiler you used)... Please try again using the proper stuff:
Your example compiles using obsolete syntax and incomplete void-safety settings indeed, but it's not very useful to debate on that. Yes, in that mode void-safety checks are extremely limited or even non-existant.<br> If you actually turn void safety on, then it refuses to let you assign Result := l_object in 'is_just', as expected (the 'check' statement is irrelevant). And you will find tons of other ways your code is wrong (from the void-safety point of view), which is precisely the point: we want the compiler to catch those errors at compile time. Even the full "void safety mode" is still in its early stages from what I understand, so there will be cases where the compiler won't detect bad cases, but it's making progress in the right direction. Void safety and assertions are largely unrelated from what I understand, besides the fact that void safety will instantly make obsolete 90% of the assertions out there (of the form 'my_thing /= Void')... Contract writers will simply have to be more imaginative than '/= Void' from now on... Other than that, there's little overlap between void safety and assertions I think. The only way I found to make your classes compile in full void safety mode is below. Start from this, and try to fool the latest 6.5 in performing a call on a Void target on an attached target (with the proper ecf settings etc of course). If you do manage to fool it, then you've earned the right to post a bug to ISE :) I couldn't find a way to fool it (tried for 10 minutes). Also, you will note that with Void safety on, most of your assertions bring no added value, because they are all related to checking that 'object' is Void or not... That check becomes moot when the compiler won't let you call Void targets anyway - you have to do better in the contracts than '/= Void' from there on... Note: I added an attribute 'default_object' because otherwise there is no way to return an 'attached G' in 'from_just' (the compiler won't let you, which again is the whole point of void safety).class MAYBE [G]
create make, make_nothing
feature {NONE} -- Implementation
make_nothing (a_default: attached G) is
-- Create as object absent.
do
default_object := a_default
ensure
no_object_present: is_nothing
end
make (a_object: attached G) is
-- Create with object.
do
default_object := a_object
object := a_object
ensure
object_present: is_just
object_set: object = a_object
end
feature -- Access
from_just: attached G is
-- Contained object
do
if attached {G} object as l_obj then
Result := l_obj
else
Result := default_object
end
end
feature -- Status report
is_nothing: BOOLEAN is
-- Is an object absent?
do
Result := (object = Void)
ensure
definition: Result = (object = Void)
end
is_just: BOOLEAN is
-- Is an object present?
do
Result := not is_nothing
ensure
definition: Result = not is_nothing
object_not_void: Result implies object /= Void
end
feature {NONE} -- Implementation
object: detachable G
-- Possible contained object
default_object: attached G
-- Default to use when 'object' is not provided
end
Defensive programming
The fact that the compiler is able to compile this code does not change the fact that the code in `from_just' looks very much like defensive programming for someone used to DbC. And what did we gain? OK, we don't have call-on-void-target exceptions anymore. But instead of that, we will silently get an object that is not the one we expected. And because this is not the expected object, it is likely that it will corrupt data somewhere else in the program. At least with a call-on-void-target the problem was reported right at the source of the problem. In my experience (again people can have a different experience), void-safety is not solving a problem, it is shifting it.
Not defensive programming :)
The thing is that 'attached G' means that the returned G is never Void. It's as if there was a postcondition saying Result /= Void all the time (no matter what the state of the object is), and it has been proven statically (as current technology allows). So, the original pre-condition stated by Colin does not really apply. You can still require 'is_just', but you still have to return an attached G no matter what, hence the introduction of a default value...
In the original snippet, it's as if you had the following postcondition: ensure is_just implies Result /= Void
But, since the return type is 'attached G', that doesn't bring any information to the table, since 'Result' is attached, and thus never Void (it does not depend on 'is_just'... it's wrong to think it does).
Arguably, void safety leads to less defensive programming than DbC. Take this example, in Colin's case you have to write this in all clients of MAYBE:if maybe.is_just then
do_something (maybe.from_just)
else
-- do something else?
end
You have to somehow verify that 'is_just' is True. You can keep repeating that requirement as much as you can in pre-conditions, but eventually, someone will have to do the 'if' above. On the other hand, when the result is attached, no one has to be defensive on this anymore. The implementation of 'from_just' has to guarantee that it returns an attached type, but all the clients are spared from being defensive on that front.
I ma be wrong because my experience with this is extremely limited, but my impression is that this is actually going to simplify our code quite a bit:
So basically, the attached mechanism brings a new added value, on top of what DbC offers: you can now state that objects are non-Void with a more powerful mechanism than DbC, one that guarantees it at compile time. You can still use DbC, but for other things than '/= Void'.
Defensive programming
The test "maybe.is_just" in Colin's example is not always necessary. It can be implied from the postcondition of the previous instruction. And we don't necessarily want to guarantee that `from_just' always returns an attached. You seem to have ignored my complaint about possible data corruption far from the source of the problem when using such pattern with a default_value.
Removing assertions "/= Void" is great. We get that thanks to the attached marker. But it is not void-safety. Void-safety is about getting rid of call-on-void-target exceptions. I'm OK to keep the attached marker, it is useful. It is the void-safety part that is causing troubles to those extensively relying on DbC.
It's good to know that 6.5 is better. I did have full void safety selected in the ECF, so apparently 6.5 is doing better than 6.4.
Colin Adams
Too ironic
I changed the ECF as you suggest, and added the -experiment option.
I didn't change the code at all - I wanted to see what would happen.
This is just too ironic - the compiler crashes with a call-on-void-target.
ROTFL
Colin Adams
You haven't submitted a bug report. On the other hand, when you add the `-experiment' option you need to recompile from scratch. The latest 6.5 was fixed in that regard and will force you to recompile from scratch.
Bug report submitted
I removed the EIFGENs directory and tried again. Same problem so I have opened problem report #16338
Colin Adams
I see void safety being equated to defensive programming but I don't see static typing being equated to defensive programming.
I don't think anyone would argue the following code is a better use of DbC than static typing:
Yes, this is a good illustration of how DbC does not make up for poor typing, and I agree: DbC can't make up for a stronger attached-mechanism-guarantee that things are not Void checked at compile time rather than at run time.
My code compiles as it stands
Except I had to change indexing to note.
This is with 6.5.8.945, and the ECF changed as you describe above (this version of the compiler doen't crash).
Again, there is a precondition violation in workbench mode (fine), and a call-on-void-target in finalized mode.
Colin Adams