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 had excluded middle.
> 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 the ciphertext. You keep trying and looking for what seems to be viable plaintext. You never get “all English strings of the given length”, because you’re not brute forcing the output, you’re brute forcing the key, which isn’t necessarily English.
If your key for OTP is uniform random bits without any additional encoding, and of the same length as the plaintext, then won't you enumerate all possible messages of the given length? E.g., "abcdef" and "123456" are indistinguishable when encrypted without knowing the key because there exist keys that map each string to the same ciphertext.
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 "base case starting at n" style proofs."
As far as drudgery, Coq will solve the trivial cases automatically, so you'd never have to prove the n = 0 case by hand. That said, there's a reason most math is done on paper and not in Coq - there's usually an order of magnitude more detail and drudgery in a formal proof, even with automation.
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 you're trying to prove for a given n is actually
P(n) := n >= 2 -> n is positive
Let's prove it by induction.
P(0) is 0 >= 2 -> 0 is positive. P(0) is vacuously true, because 0 < 2.
Suppose P(n). We want to show P(n + 1). Our goal is
n + 1 >= 2 -> n + 1 is positive. Let's break this into the cases n >= 2 and n < 2.
For n >= 2, we assume P(n) and have the LHS of the implies. This gives us n is positive. Say by definition or by a lemma that n positive -> n + 1 is positive, and we handle this branch.
For n < 2, the inductive hypothesis tells us nothing. Assume the LHS of our goal, i.e. n + 1 >= 2. We want to prove n + 1 is positive. Well 2 is positive and therefore n + 1 is positive by transitivity.
This is what I mean by the base case not being special. E.g., in Coq, induction over the natural numbers always starts at 0. When you think about doing induction starting at another number, you're transforming your goal to include something of the form n >= m -> P(n).
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, you work the base case into the goal, like n >= 2 -> P(n). Then you do the base case as part of a branch in the inductive step, without using your inductive hypothesis.
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 of size two, your inductive hypothesis is not sufficient to prove that h1 and h2 are the same color.
Saying it's the base case that's wrong is a little weird. In general your base case can be vacuously true without any issue. However, if it is (and your goal is non-vacuously true for something), then your inductive step will require a branch in it. One side of the branch in your proof will look like a proof of a base case.
I have maybe a skewed view on this from using Coq.
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.
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.