It’s not just [] - it’s any amount of leading 0s.

But this is exactly the point - if you forgot about proving `ToBytes(FromBytes(bs)) == bs`, forgot about this edge case, and later tried to prove a function that implicitly relied on that fact - Dafny would let you know!

This also sounds like CouchDB: https://couchdb.apache.org/

27k / 540 = 50

Or they’re true AI believers, and believe AI assisted chip design will erode NVIDIA’s edge

Source for magnitude of negative externalities?

This would be way clearer as a Cartesian plot with the output of random as X, and sample number as Y.

The target block time is 10 minutes, and you need to wait multiple blocks to be confident you’re really on the longest chain

That’s the joke :)

If I autogenerated a huge amount of C based on the weights, that added/multipled variables the same way the existing code+weights does, then would it be “source”?

https://certificate.transparency.dev it is

Thanks, I was not aware!