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…
> 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…
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…
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…
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,…
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…
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…
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 combinators, but if not, that could be a…
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…
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 small ASCII diagram in the comments, and…
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…
TrueType font hinting actually is Turing complete. A font may contain programs that run on a VM that has functions, variables, unbounded loops, etc.
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…
> 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…
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…
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…
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,…
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…
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…
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 combinators, but if not, that could be a…
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…
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 small ASCII diagram in the comments, and…
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…
TrueType font hinting actually is Turing complete. A font may contain programs that run on a VM that has functions, variables, unbounded loops, etc.