assert semantic change proposal

[Ola Fosheim Gr via Digitalmars-d]

On Tuesday, 12 August 2014 at 14:43:23 UTC, Kagamin wrote:
> A proof usually flows from causes to consequences, the reverse 
> (induction) is ambiguous.

If a deterministic imperative program is ambigious then there is 
something wrong. So no, ambiguity is not the problem. The size if 
the search space is. The preconditions are "the ambiguity" which 
the theorem prover try to find...

> Ordering is more fundamental: you can define or redefine it, 
> but it will remain, one can't think outside of this formalism.

Explain.

>> Not at all. You can create a boolean expression for every bit 
>> of output and evaluate it only using NAND gates (or NOR). Not 
>> practical, but doable…
>
> Mathematics is pretty aware of differences between algorithms, 
> and proving their equivalence is non-trivial.

Define non-trivial. We were talking about the nature of finite 
computations. They are all trivial. Algorithms are just 
compression of space.