vyodaiken

Nobody wants that.

Exactly. You are assuming that a poorly written standard is correct and engineering practice of working programs is incorrect.

C programmers should be able to expect that "optimizations" will not transform program meaning. And because C is so low level, certain types of optimizations may be more difficult or impossible. If the pointer was explicitly set to NULL, the compiler can justifiably deduce the branch will not be taken but the deduction "if the programmer dereferenced the pointer it must not be NULL" is not based on a sound rule. In fact, the whole concept that the compiler can make any transformation it wants in the presence of UB is wacky. Optimization should always be secondary to correctness.

It's easy to see the problem in the null pointer case. The compiler deduction is that the null test is redundant, but it's not actually redundant. Therefore the compiler "proves" a false theorem. That the standards rules permit the compiler to deduce false things would be, in normal engineering analysis, considered to show a failure in the rules, but the bureaucratic mindset holds that the rules are always, by definition, correct, so the failure is the fault of the miscreant who neglected to staple cover sheet properly.

If the compiler is unable to prove a transformation preserves correctness, it should not do the transformation.

To your point below: The compiler is definitely not "forced" to assume that the pointer is not null - that is a choice made by the compiler writers. Even the ridiculous standard does not require the compiler writer to make that assumption. The compiler can simply compile the code as written - or, if it is smart enough to see the problem - it can produce a warning.

This is not really correct. The kinds of implementation dependencies usually encountered reflected processor architecture. The C standards committee and compiler community have created a situation in which different levels of "optimization" can change the logical behavior of the code! Truly a ridiculous state of affairs. The standards committee has some mysterious idea I suppose, but the compiler writers who want to do program transformation should work on mathematica or prolog, not C.

If you are going to do theorem proving, you should try to only prove true theorems.

This is a kind of Department of Motor Vehicles Bureaucrat thinking. For example, there as many thousands of lines of C code that reference *0, which is a perfectly good address in some environments. One should be able to depend on compilers following expressed intentions of the programmer and not making silly deductions based on counter-factual assumptions.

It's a stupid convention of compiler writers and standards writers at the expense of common sense and engineering standards. In fact there are many thousands of lines of C code that depend on compilers doing something sensible with UB. For example 0 is a valid address in many cases (even in some versions of UNIX). The decision to allow compiler writers to make counter-factual assumptions on the basis of UB is the kind of decision one expects from petty bureaucrats.

Correct. The X axis is our estimate of actual time from GPS time. The Y axis is the deviation from estimate. The estimate includes a slew of about 5 minutes around the leap second.

You missed my point. Probably I expressed it poorly.

I gave a reference to Feynman's note. The "stateful calculating agent" is the physicist or student.

In a physics lecture, the audience is reasonably smart but slow - so you can use compact natural language flavored instructions: e.g. "as we take the limit of x to zero, expression(x) goes to c" which change values of variables. In programming, the agent being addressed is analogous to Turing's dumb schoolboy - it's very literal and needs easy to interpret instructions for each step so: c "= trytocomputelimit(f,x)". In both cases, the state of the calculating agent changes as it follows the steps of the calculation.

I randomly open Feynmans lectures on physics and see

E (between the sheets) = sigma/epsilon0

E (outside) = 0

assigning two different values to the variable E.

In applied math, there are many expressions in which a variable y is treated as a value (depending on implicit parameters) or as a function y(t) depending on explicit independent variables. This is a matter of convenience, not principle.

I think that's a basic misunderstanding of mathematics and physics that is often used as a justification for functional programming. Formulas in physics often reference implicit state such as the time - which is exactly what imperative programming languages do.

I'm agreeing with you about the difference of perspective.

These lists all leave out the most critical security fact: the official state department email system was grossly insecure and was compromised by Russian hackers. This fact makes all the other stuff seem silly.

Some thoughts on consensus algorithms, why Paxos is so tricky, and a reminder of the Chang/Maxemchuk algorithm.