Have a sneer percolating in your system but not enough time/energy to make a whole post about it? Go forth and be mid - welcome to the Stubsack, your first port of call for learning fresh Awful you’ll near-instantly regret.
Any awful.systems sub may be subsneered in this subthread, techtakes or no.
If your sneer seems higher quality than you thought, feel free to cut’n’paste it into its own post — there’s no quota for posting and the bar really isn’t that high.
The post Xitter web has spawned so many “esoteric” right wing freaks, but there’s no appropriate sneer-space for them. I’m talking redscare-ish, reality challenged “culture critics” who write about everything but understand nothing. I’m talking about reply-guys who make the same 6 tweets about the same 3 subjects. They’re inescapable at this point, yet I don’t see them mocked (as much as they should be)
Like, there was one dude a while back who insisted that women couldn’t be surgeons because they didn’t believe in the moon or in stars? I think each and every one of these guys is uniquely fucked up and if I can’t escape them, I would love to sneer at them.
@lagrangeinterpolator@awful.systems @dgerard@awful.systems To add a note on computer verifiable proofs, a story from my own PhD (Cryptography).
It was the night before either the submission-deadline or the deadline for the rebuttal for PQ-Wireguard. Andy and Peter had already retired for the night, basically announcing that they would do the final touches in the morning, with Kai-Chun and me instead working late to finish some TODOs and in exchange being done the following day.
I pretty much got most of the stuff I had been working on done and moved to the Tamarin proofs for some editorial work there and noticed that a statement, for which we had a Tamarin verified proof didn’t seem to make sense. As in: I could give a counter-example in the form of an instantiation of PQ-WG, where that property would be trivially not there! (I believe it was anonymity and that trivially doesn’t hold for any KEMs where the ciphertext reveals the public key, which is not something that is at all incompatible with standard KEM-notions.)
Turns out: Tamarin works in an idealized model and what the proof actually meant was more akin to “There is nothing fundamental in your model that prevents PQ-WG from having that property if you instantiation doesn’t add problems there”.
Which is a very different statement of course!
The end of the story was basically that we called out supervisors late at night, when their work-days really were meant to be over and they wanted to spend time with their partners, that the house was on fire and what we should do.
IIRC the final version of the paper mostly states something along the lines of “it holds if the KEMs don’t leak it”, but the important thing here is that this was computer-verified, just in a model that turned out to be insufficient.
And no, I don’t think anyone here did anything wrong. When I approached Cas Cremers with the issue later his response was also kinda “yeah, symbolic models really struggle in that area”.
And furthermore: I am the last person to deny the need for computer-verifiable proofs, textual proofs have turned out to be disasters, but we really need to be aware of what can go wrong and what they mean.