Bad ideas in type theory


Types as sets and subtypes as subsets.  This may be due to confusing usage in mathematical practice where, for example, we often see references to integers as a subset of reals. But in mathematical usage, people generally understand that while real numbers without fractional parts are a subset of the…

Current reading: July 8 2017


Principal type-schemes for functional programs∗ Luis Damas† and Robin Milner First published in POPL ’82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, pp. 207–212 THE PRINCIPAL TYPE-SCHEME OF AN OBJECT IN COMBINATORY LOGIC BY R. HINDLEY Quicksort.  Tiny C - sheer genius! Plan B …

The C standard committee effort to kill C continues


Consider the following code: void f(void) { unsigned char x[1]; /* intentionally uninitialized */ x[0] ^= x[0]; printf("%d\n", x[0]); printf("%d\n", x[0]); return; } In this example, the unsigned char array x is intentionally uninitialized but cannot contain a trap representation because it has a character type. Consequently, the value is both indeterminate and an…

Chang-Maxemchuk atomic broadcast


The Chang-Maxemchuk algorithm (US Patent 4,725,834 ) solves atomic broadcast (and in-order broadcast) problems for distributed networks in a far simpler and more efficient way than some popular alternatives. In fact, the obscurity of this method is hard to understand given the current interest in distributed consensus. The basic idea is simple…

Making Paxos face facts


Lamport's  "Paxos Made Simple" paper is notoriously hard to understand but at least part of the difficulty is that the algorithm  changes radically in the middle of the presentation.  The first part of the paper presents a subtle (maybe too subtle) method to permit multiple processes or network sites to agree…