eperdew

5 ms·

1.
by eperdew 4y ago
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 separation logic based provers I've used have all
2.
by eperdew 5y ago
> 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 ciphertext. So your key is a binary blob the same length as
3.
by eperdew 5y ago
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. I think this is something that is not clear if you just do &
4.
by eperdew 5y ago
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 for all n >= 2, n is positive. The statement y
5.
by eperdew 5y ago
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 "picking a base case" that's sufficient, y
6.
by eperdew 5y ago
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. The problem is (as mentioned in the article), that for sets
7.
by eperdew 5y ago
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 bit more time parsing the expression for no gain as a reader.
8.
by eperdew 5y ago
This is why the aliasing rules in C explicitly allow aliasing any pointer type with a char*.
9.
by eperdew 5y ago
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.
10.
by eperdew 6y ago
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 combinators, but if not, that could be a potential pe
11.
by eperdew 6y ago
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 asking because I was just making this decision the other
12.
by eperdew 6y ago
Thank you for the explanation. This is a very comfortable level of detail in my opinion, if you were to write a full article.
13.
by eperdew 6y ago
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 small ASCII diagram in t
14.
by eperdew 6y ago
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 null out the next field so that you don't a
15.
by eperdew 6y ago
TrueType font hinting actually is Turing complete. A font may contain programs that run on a VM that has functions, variables, unbounded loops, etc.