On Monday, 19 May 2014 at 18:55:57 UTC, Steven Schveighoffer
wrote:
On Mon, 19 May 2014 14:49:41 -0400, Ola Fosheim Grøstad
<[email protected]> wrote:
On Monday, 19 May 2014 at 18:33:55 UTC, Steven Schveighoffer
wrote:
Then you should have no problem producing an example, right?
I did. Besides, I think language constructs should be proven
sound a priori, not post mortem...
Let me cut to the chase here. I haven't seen it. Let's not go
any further until you can produce it.
I've given several examples, but I oppose the general attitude.
Language constructs should be formally proven correct. Proving a
program to be correct is usually not worth it, but for individual
language construct it is indeed possible and necessary,
optimization depends on it. This is also why you should strive
for a small set of primitives and build high level constructs by
lowering them to the minimal language. You can then limit your
proof to the primitives.
The basic idea in generic programming is that you can implement
the full blown generic algorithm, plug in the parts that can vary
and let the optimizing compiler boil it down into an optimized
tight machine language construct. The programmer should not be
required to "deduce" what will happen when he plugs stuff into
the generic algorithm.
If optimization change semantics you will risk efficient
algorithm implementations either going wrong or into an infinite
loop. Not at all suitable for a programming language that aims
for system level efficiency and generic programming.
