5 ms·
One other way to prove these algorithms is by writing them in z3 prover. You write a simple one that is 100% correct and then you prove equality for your optimi
by knuthsat 5y ago
One other way to prove these algorithms is by writing them in z3 prover. You write a simple one that is 100% correct and then you prove equality for your optimized one or find an example that will show inequality.
- chrisseaton 5y agoA great thing about a monadic operation that takes a 32-bit integer, like this one, is that you can also just exhaustively test it in reasonable time!
- Dylan16807 5y agoToday I learned "monadic" has two significantly different meanings in the realm of programming. I'm only familiar with using "unary" to mean single-parameter.
- Filligree 5y agoNah, they’re pretty much the same meaning.
- Dylan16807 5y agoA monad, derived from monoid, means multiple very specific things completely unrelated to the other definition of "single parameter". And the etymology is basically a coincidence because "mono" got used in different places, isn't it?
- a1369209993 5y ago> []completely unrelated[] to the other definition of "single parameter". Actually, all monads are monadic functions/operators on their (usually type) parameter. Eg, 'list' is a monadic operator from element types to types of lists of those elements. It's completely different (AFAICT), and mostly unrelated, but it's not completely unrelated.