domenic at domenicdenicola.com (2013-07-17T18:54:12.742Z)
On 10/07/2013, at 03:49, Mark S. Miller wrote: > Because Nat includes 2^53, this code actually fails to enforce conservation of currency!! I've repeatedly claimed this conservation property about this code and code like it for a long time now, to many audiences and in several papers. There have been several exercises proving some properties of this code correct and laying the groundwork for proving conservation of currency. However, none have previously spotted this hole. Right, if balance+amount ever result in 2^53+1, the code would rather "see" it (and save it!) as 2^53. Sort of a new kind of off by one error... for the wikipedia?
On 10/07/2013, at 03:49, Mark S. Miller wrote: > I initially didn't think this mattered, but it is an excellent and important point. Look at the use I make of Nat in Dr.SES in Figure 1 of <http://research.google.com/pubs/pub40673.html>: > > var makeMint = () => { > var m = WeakMap(); > var makePurse = () => mint(0); > > var mint = balance => { > var purse = def({ > getBalance: () => balance, > makePurse: makePurse, > deposit: (amount, srcP) => > Q(srcP).then(src => { > Nat(balance + amount); > m.get(src)(Nat(amount)); > balance += amount; > }) > }); > var decr = amount => { balance = Nat(balance - amount); }; > m.set(purse, decr); > return purse; > }; > return mint; > }; > > Because Nat includes 2**53, this code actually fails to enforce conservation of currency!! I've repeatedly claimed this conservation property about this code and code like it for a long time now, to many audiences and in several papers. There have been several exercises proving some properties of this code correct and laying the groundwork for proving conservation of currency. However, none have previously spotted this hole. Right, if balance+amount ever result in 2**53+1, the code would rather "see" it (and save it!) as 2**53. Sort of a new kind of off by one error... for the wikipedia? -- ( Jorge )();