Viewing profile — eperdew

Yes - to elaborate, a constructive logic is a logic without P or not P. This doesn't have much to do with whether a tool can tell you what obligations you haven't proven. The separ…

> To attack classic OTP, you’d brute force the keyspace. Since we’re XORing, whatever we encode the key as, it’s fundamentally being used in binary to XOR between plaintext and cip…

I wrote out quite a bit for this, but I think that the main point is that by falling back to the formalism, we see the the LHS of the implication affects our inductive hypothesis. …

The example I'm about to give is overkill, but I'm trying to make my point very carefully. Suppose you want to prove something for integers >= 2. E.g., suppose you want to prove fo…

You don't have to. See my top level comment. In short, you have to strengthen your goal in order to have a strong enough inductive hypothesis to prove anything. E.g., instead of "p…

I started to write out what is happening here more formally, but I think it was not very elucidating. No matter what, the problem is that the proof of the inductive step is wrong. …

To me, adding parentheses when using common operators signals that I should read it carefully, because normal precedence is probably broken. When that is not the case, I spend a bi…

This is why the aliasing rules in C explicitly allow aliasing any pointer type with a char*.

Agreed. I alleviated this in my last zig project by just declaring a type alias, however. Strings could use some nice support from the stdlib once it gets fleshed out.

I'm not sure if this is done in practice, but in theory, if you compile a regex to a DFA, you can then minimize the DFA. I don't know if you can do anything similar with parser com…

There are some features exclusive to errors though (errdefer, stack traces, implicit error unions). Did you find yourself missing any of these by doing it this way? I'm partially a…

Thank you for the explanation. This is a very comfortable level of detail in my opinion, if you were to write a full article.

All pointers are pointers too, so I don't see much of a difference between "indirect" and "next_ptr", other than the "next" part. In similar situations at my job, I've drawn a smal…

As others have said, often you don't want to free the node, you want to do something else with it. E.g., put it in a free list. However, usually if you're not freeing it, you'd nul…

TrueType font hinting actually is Turing complete. A font may contain programs that run on a VM that has functions, variables, unbounded loops, etc.