Victor Yodaiken

Some of those are classics. The Lipton-Perlis-DeMillo argument against program verification is a good one.[1] They demonstrated that manual programming verification via hand theorem proving is buggy. Automated theorem proving was new back then.

This was an issue back in the 80s for a philosophical reason in mathematics. Mathematics classically approves of short, clever, elegant proofs. The paper-and-pencil crowd was trying to do that for code. In practice, program verification is about mechanized grinding through massive numbers of dumb assertions to catch off-by-one errors.

This used to bother mathematicians. When the four-color theorem was originally proved, it was done partly by hand and partly with computer case analysis. The computer part bothered many mathematicians. The culture has changed. Recently, someone redid the proof with the old hand parts re-done by computer. Since that eliminated some possible human errors, that was a step forward in solidifying the proof.

We also know now how to check a theorem prover. Some theorem provers emit a proof trace, huge files of "Step 2437: apply rule 42 to change 2*X to X+X". Proof traces can be fed into a dumb proof checker which does the indicated rewrite and checks that the expected output is obtained.

So progress has resolved that issue.

[1] http://www.yodaiken.com/papers/p271-de_millo.pdf

All I can do is point out that very big names in CS (including Linus) disagree with you: http://www.yodaiken.com/wp-content/uploads/2018/05/ub-1.pdf

This is probably because they’ve seen the effects of the foot gun first hand. They also recall what C/C++ looked like before the standards bodies made exploiting UB in compilers open season. There’s also a reason why Rust doesn’t have any UB in its safe dialect even though it sits on infrastructure capable of most/all the same possible optimizations via LLVM.

There was in fact a direct kernel security issue UB exploitation caused in the Linux kernel whereas without that optimization there is no security issue. if I recall correctly the code looked something like:

Some_value = ptr->value
If (!ptr) { return; }

This worked correctly in all cases before the compiler added the optimization. It worked less well after because the !ptr check was UB since it followed a dereference. It also wasn’t immediately obvious this code was broken because there was no diagnostic nor any indication that upgrading a compiler would suddenly elide the check. The value-add of such optimizations at scale vs the correctness issues exploiting it causes is questionable.

The problem wasn’t that it’s not fixable. It’s that it takes time to find and you may not even find it until after it’s being exploited.

[Edit: this isn't true] That is definitely how it is used, and it works on the major compilers. But, surprisingly, this is indeed undefined behaviour according to the standard. There was an infamous rant by Linus [1] (more infamous for the language than the subject) about how the kernel can and should continue to use unions for type punning. He noted that even though the C standard doesn't specify a behaviour for that usage, gcc does (so long as you don't use a particular compiler switch mentioned in that discussion), and went on to say "The standard simply is not important, when it is in direct conflict with reality and reliable code generation."

EDIT: Having looked into this more I think I was getting confused with C++ (where the only supported way to type pun is to use memcpy or similar, which despite the name might not have to actually copy the bytes at runtime). Here [2] is a StackOverflow answer (/discussion) on the matter.

[1] https://www.yodaiken.com/2018/06/07/torvalds-on-aliasing/

[2] https://stackoverflow.com/questions/25664848/unions-and-type-punning

Yeah, I think a degree of complexity is required to achieve being the fastest compiled language.

To achieve that, you need stuff like monomorphized templates, actual arrays and slices being distinguished from pointers, well-defined rules on pointers (like Rust's rules about references and mutable references, or strict aliasing in C++), and the freedom to let the compiler reorder structure fields for better alignment and space usage. Runtime polymorphism, like virtual functions in C++, are better as a core language feature rather than something implemented as a struct of function pointers, because that way the compiler can devirtualize some calls.

All of these things, I think most C programmers would be against adding to C. And pointer rules are historically controversial; for example, Dennis Ritchie was against adding noalias to C in 1988[1].

[1]: https://www.yodaiken.com/2021/03/19/dennis-ritchie-on-alias-analysis-in-the-c-programming-language-1988/

The standard massively conflicts with the practices used in existing C programs by existing C programmers. Yes, it's perfectly possible to write code that doesn't violate any of the (largely implicit, it's worth noting) strict-aliasing rules. But was it a good idea for the standard to allow optimizing compilers to silently break massive amounts of existing code that has worked for years? Even if that were acceptable, was it a good idea for the standard to disallow one of the more ergonomic and explicit ways (using a union) of reinterpreting an object as an object of a different type?

Some good reads on this topic:

https://blog.regehr.org/archives/1307

http://www.yodaiken.com/2018/05/20/depressing-and-faintly-terrifying-days-for-the-c-standard/

https://blog.regehr.org/archives/903 (See the end of Xavier Leroy's comment)

This is authentically a very interesting simulation and I would be interesting to see a writeup if you have one. I will say that you only have multiple proposers if the proposers cannot talk to one another, as otherwise they would be silenced by any simple leader election protocol (heartbeats + node rank, etc.) It's true that the leader election protocol is not part of paxos per se but all implementations will have one, and the protocol livelocks in the unusual case where there's an enduring network partition and the multiple proposers are sending messages with specific timing.

Edit: I took a look at your post[0] and it is interesting. I'll take a look at CM.

[0] https://www.yodaiken.com/papers-and-talks/distributed-consensus-paxos-raft-etc/