3 ms·

But the language can't prove that. In the paper they show that it thinks the output is mixed until you add a manual assertion telling it to simulate the thing t

• amluto 5y ago
  It’s also an odd feature of a programming language. Imagine the classical equivalent: square : constant integer -> constant integer square(2) is 4. square(4) is 8. square(readint()) doesn’t compile because readint() may return a mixture (if, say the user rolled a die and entered the result on the keyboard), so the input isn’t pure and you can’t square it. This is, of course, almost useless. (Amusingly, gcc can do this. asm’s "i" has precisely this restriction. Use with caution.)