saithound

32 ms·

361.
by saithound 7y ago
Both features went one way. Comprehensions were introduced in the functional language Miranda (and to a limited extent its predecessor KRC) back in the 1980s.
362.
by saithound 7y ago
TLC checks models, not implementations, so the compariaon is not really appropriate at all. Using TLA+ on actual code is yet to be a success story: Deductive methods the assembly refinement proof of seL4 (binary verification) is completely
363.
by saithound 7y ago
> You can buy off-the-shelf model checkers that do more in industry pretty much all the time. When you establish actual deep properties, that's news. You can't buy any model checker that verifies confidentiality for actual kern
364.
by saithound 7y ago
> The same ones that formal methods research focuses on (for deep properties): model checking and concolic testing, which have shown much better scalability than deductive methods Model checking is great, and many tools developed by the
365.
by saithound 7y ago
You implied he was premature, a perpetual victim, and asked loaded questions implying he can't get laid. By trying to belittle and demean him, you ended up strengthening his point. I can't fathom what you tried to accomplish by lo
366.
by saithound 7y ago
It does not. Feel free to justify your claim by writing down an explicit counterexample, though.
367.
by saithound 7y ago
> Also, it's not clear to me that your proposed wraparound addition operator is actually fully associative in all possible cases of overflow. Proof sketch: write out (an/ad + (bn/bd) + cn/cd)) and ((an/ad + bn&#x
368.
by saithound 7y ago
> This definition is not complete. What happens when "bd x ad" is larger than the maximum allowed denominator ? All integer operations are twos complement operations, as I'm sure you guessed anyway. > the overwhelming m
369.
by saithound 7y ago
> It does not preserve associativity of addition. It does, if you use the mathematically natural addition operation (see my reply to enriquto). In the example above, the result is MAX_INT/1 in both cases.
370.
by saithound 7y ago
> I do not see how this can possibly be the case. How do you define rational arithmetic with bounded denominators so that addition is associative? There's only one mathematically natural choiceIn the case of bounded numerator and bo
371.
by saithound 7y ago
It is not at all the same situation as with floating point numbers. 1. It does not use a predetermined finite set of rational numbers. It uses a bigint numerator and a 64-bit denominator. 2. Even the case of bounded numerator and bounded de
372.
by saithound 7y ago
Von Neumann was thoroughly familiar with non-classical logic. He himself came up with several variants (including quantum logic) in the 1930s.