fdupress

Etam absolutely allows you to authenticate an unencrypted context. In fact, you must ensure that the nonce, a piece of unencrypted context, is authenticated. Nothing stops you from throwing more stuff in there.

The only thing you can do with an integrated AEAD that you can't do with a constructed one (with standard interface and security) is include authenticated and unencrypted context halfway through an encryption.

The pattern is the same on every card, but the cards are cut in a way that doesn't align with the pattern, so the two edges of a card don't look the same.

It's still a manufacturing defect, which could be sorted out by paying more for those decks that are to be used in higher stakes games.

Not if every single one of its posts gets linked.

Hash the input (O(n)), search for a second preimage (very much not O(n) if you use a cryptographic hash).

No, sorry; I'm not aware of proper comparisons for C verification tools, or at least recent and maintained tools.

SV-COMP tends to propose a huge number of relatively simple tasks, which attracts model checkers and static analysers. Frama-C and VeriFast are functional verification tools. You can use them as static analysers, but there's a barrier to entry in terms of minimal required annotations that might not be present for tools designed for static analysis.

You could also try VeriFast [0], which is closer to Frama-C than CBMC. (VeriFast and Frama-C are deductive verification tools, CBMC is a bounded model checking tool.)

It is slightly less approachable than Frama-C because it uses separation logic, but it's slightly more approachable because it uses symbolic execution, which allows it to display an actual execution trace that causes the failure. (You can then inspect that and decide whether your code or model is wrong.)

[0]: https://github.com/verifast/verifast

Rejection sampling works when your bias is constant, not when it varies depending on the environment.

Space might be a good enough approximation of energy to not bother?

By the definition you link, combined with its subdefinition for uncountable, finite sets are uncountable.

That is a pretty big leap from accepted terminology.

Thanks for your comment; learned a couple of things.

Sorry, I was more careful in my second mention of "the set of real numbers". Thoughout, I meant "the set of real numbers that arise from set theoretic constructions".

In other words, the object on which the existing proofs of uncountability hold and the object constructed in the talk are not necessarily the same object. In fact, the care taken by Bauer in clarifying "the object of Dedekind reals" in stating his main results leads me to believe the topos in which the Dedekind reals are countable is also a topos in which the Dedekind reals are not equivalent to other constructions of the reals.

Just a quick addition: note the care taken to avoid using the word "set" in your excerpts. My objection was with the submission's current title ("The countable set of real numbers"). It still stands.

That is an assertion about one particular construction of the reals, in a particular topos, which implies something on the constructed set in that topos.

I'd argue that that set, resulting from carrying out Dedekind cuts in a particular topos, is not in fact the set of real numbers. But I also agree that it means the property of uncountability for the set of real numbers as we understand it in set theoretic terms cannot be proved intuitionistically. And I'm fine with that.

The title of the video and talk is "The countable reals."

There are plenty of countable sets of real numbers (Q and all its subsets, for one infinity), and the set of all real numbers is not countable, so there is no interpretation of the current submission title that makes sense.

Strings/lists under concatenation do not form a group since concatenation is not uniquely invertible. (In the sense of "there is no list -xs that you can concatenate onto xs to get the empty list.)

I don't think the charge needs to be unattractive to spammers to mitigate the costs associated with them: 1$ likely covers the CPU time to produce the page, and then it only costs when displayed (which will be little, if spam).

Enormous future potential for derivative work gets created. Enormous future potential for original work gets erased.

Why would anyone in their right mind choose to put effort into creating original art if there is "one easy trick" to get around copyright by simply turning their art into a model that can be used to churn out things they could have produced?

And that reason is that there is a canonical definition of what it means for two numbers to be equal.

The fact that your intuition of "these two timestamps are equal" is "these two timestamps denotes the same instant" seems problematic when we know that the notions of timestamps and time are not in fact aligned (because, for example, of leap seconds).

> As we see from Japan and other countries, wearing a mask can keep much of the goo that comes from sneezing and coughing policed. It’s not perfect but it protects others and thus it’s polite. It’s also a reminder to not touch one’s face quite so readily.

I'm not entirely sure if this is a mistake or if there's a deep hint of an equivalence between masks and (lack of?) transparency; and between goo and salaries.

Take a look at this one (also NSFW) https://pornpen.ai/view/CBHr5AlP8AFAZ56Jkp7i

Arguably, if the court ends up agreeing that you did have an account and that Valve needs to give control of it back to you, would that not be evidence that you had agreed to the terms, then broken them by rejecting arbitration? (Leading to Valve being able to take your account away because you broke the ToS.)

Sure, but you get probably correct code out of it. Not every productivity increase has to do with quantity.

It seems to me that "a lot of uncertainty going around for years" would make some attempt to actually set up a buffer to better absorb shocks and adapt. This is not about predicting the future, it is about failing to manage a clearly increased risk of failing to predict the future.

Looked for it and missed it.

And thanks for writing this up, by the way. Having people less familiar with formal methods try and write up their experiences is, I think, much more effective at letting people in than having experts try and write tutorials.

Every time somebody proves that a sorting algorithm sorts, they forget to prove that the algorithm doesn't just drop values or fill the entire array with 0s (with fixed-length arrays, as here).

On paper: "it's just swaps" Formally: "how do I even specify this?"

(For every value e of the element type original array and the final array have the same number of occurrences of e. Show that that's transitive, and show it's preserved by swap.)

Wait... A bridge built for bicycles only to go over still needs cars and lorries and other large things going under it.

A bridge built for bicycles only to go under is nice, and means not even having to deal with a slope. (But might be more costly than a bicycle tunnel.)

Those are important design-level tasks, and are in fact some of the tasks discussed by the linked video...

The hotcrp conference management system treated it as a shell glob and leaked out the list of submitted papers, once.

Vaccines go into muscle, not blood vessels.

It's still much better for everyone involved to not stick air into your muscle, though.

Hey there. I read this as "a fun-free platform" and was very confused for a bit. You might want to reconsider the order of your adjectives.