As I said in another comment, individual verifiability and non-coercion are mutually exclusive online. However, there are indeed solutions for the other properties (including global integrity), and compromises between individual verifiability and non-coercion. For instance, you can have a look at Helios [1] or Belenios [2]. Current research is looking for stronger guarantees, a better compromise, or a more interesting voting system (such as Single Transferable Vote or Majority Judgment).
That is indeed the main issue with verifiable voting. The usual solutions offer various compromises, but it is not possible to both guarantee the ability to verify that one's ballot is counted correctly, and that you cannot prove for whom you voted.
> That's only possible if you sacrifice some of the stronger anonymity requirements
Untrue. You can use strong encryption to ensure confidentiality and zero-knowledge proofs to ensure integrity. Then, you can use methods from homomorphic encryption to tally the ballots. There is a whole area of research dedicated to this.
"Automated proof" means that the verification is automated. Actually automating the process of finding proofs is still mostly an open problem.
Formal proof software will help you on small stuff, but you will still do most of the work, and you have to go much more in details, so it takes much more time.
> When you try to come up with random words to compose a password
That's why you don't. Give a 64ki word dictionary from your native tongue to your computer and let it choose four words uniformly at random out of it. This gives you a password from a distribution with 64 bits of entropy, and is reasonably easy to memorize with moderate effort.
This means an attacker is expected to proceed to 2\\63 hashes to crack such a password. It would take almost 4 year to crack its MD5 digest on the rig used in the demonstration. If you not using a password manager for external sites (which might not use proper KDFs), you can throw in a fifth word, and be safe for the foreseeable future.
Right, my bad. I tend to write loops in the former style, thinking of them as reversed(range(9)). This is another advantage of this style. I should have been more cautious when writing the second one.
The point is that a beginner does not need to care about signedness. When you get to that point, you can take the time to explain how to loop properly over it.
This is about weighing correction versus readability. In the "arrow operator" version, the readability is decreased; in the "proper" version, a type cast is required, and this can lead to bugs with values greater than 2^sizeof(ssize_t).
Obviously, I just follow the convention when contributing to an existing project.
You are talking about making a combined hash function from MD5 and SHA-1. Keep in mind that it is not trivial. For instance, if you just output both SHA-1 and MD5, you are actually only as strong as the weakest hash function (trivially for preimage, but also true for collisions, see [1]).
If you are interested in hash function combiners, have a look at Robust Multi-Property Combiners for Hash Functions [2], a recent paper on the topic. It aims at getting several properties at the same time (preimage resistance, collision resistance). For simpler schemes with a single property, just explore the bibliography at the end of the paper.