spectrums_coherence

the cryptography module has unit tests and formal verification.

Did you develop the spec by hand or is AI also involved in the spec development?

As far as I am not pleased with garbage proofs that these AI likes to write, it is still better than garbage spec…

I suspect your formal proof refers to the following files: https://github.com/positive-intentions/signal-protocol/tree/staging/formal-proofs

It contains 6 files each with less than 100 lines of code, and the claim seems to be it almost prove the entire security of the signal protocol.

Unless the formal proof community has advanced so much without me knowing, then I think you can definitely submit a paper to top PL conferences. Since my best known state of the art is Signal* from project everest. It involves tens of components, and years of works for top academics and proof engineers.

• Here is the website: https://project-everest.github.io/
• Here is the paper: https://www.computer.org/csdl/proceedings-article/sp/2019/666000b256/1dlwheTvbEI
• Here is the code: https://github.com/Inria-Prosecco/libsignal-protocol-wasm-fstar

Each file here, like fstar/Impl.Signal.Core.fst would already be longer than your entire proof, even just the hints provided to the SMT solvers are longer than your entire proof.

So I am interested in what technique did you apply to acheive the almost same effect as this monumental project with less than 5% of the code?

Boy, you thought blocking ml and hexbear is enough to get away from this bullshit. Sigh…

Yeah, unfortunately my class do not train student in essay writing. I do require students to write a proposal for their project which details the motivation and spec of their project. I feel a large amount of them are mostly not AI written.

While it is very easy to trick chatgpt 3.5 into submission, modern models, especially paid ones are hard to trick while not giving students without AI an disadvantage.

So the alternative is making the class very verbose and/or require much deeper understanding and novelty that is beyond the scope of a introductory class (which most undergrad/grad classes are).

For now, what I am doing is just making the homework optional or worth very little, and grade based on exams, quiz, participation, and projects. Since everyone will get perfect score on homework anyway, so there is no point in evaluating that nowadays :(

I tried it for my class, and the questions they come up with is boring, repetitive, and generic.

I feel very sorry for you that you need to endure that.

Amos Bar-Joseph, CEO of Swan AI, bragged about his Anthropic bill in a viral LinkedIn post, saying “We’re building the first autonomous business - scaling with intelligence, not headcount.”

Given how unintelligent this sentence is, maybe using LLM is indeed the more intelligent choice for them after all…

I am sure food company, dietitians, nutritionists, and companys that offer weight management products will beg to differ.

I would be really cautious in giving any biometric data to OpenAI.

I still remember the good old days when google has the best code quality among big techs. That being said, seeing how shitty everyone’s code has become, google might still be the best :)

I am sure in 30 years there will be plenty of Americans worship Trump just like they are doing now to Reagan.

Even though both of them fucked literally everything up.

fuzzy foxy

I believe they are higher dimensional string diagrams. Maybe called n-diagrams? They are used in higher homotopy and higher category theory, I believe. But not entirely sure.

https://arxiv.org/pdf/2305.06938

EDIT: Found it! they are called surface diagram, which are generalization of string diagram to 3-categories https://golem.ph.utexas.edu/category/2010/03/modeling_surface_diagrams.html https://ncatlab.org/nlab/show/surface+diagram

Still not sure what the proof is talking about though :(

But from the conclusion it looks like some sort of natruality condition, where the morphisms are slided around except beta.

EDIT AGAIN: got in touch with my string diagram contact. Here is the paper https://arxiv.org/pdf/0807.0658

Note the conclusion at the bottom, the proof on the right and the axiom on the left doesn’t seem to be related.

The proof on the right is Theorem 6; the equality at bottom is in section 3.4, where the proof is omitted because “follows from definition”; the axiom on the left is HM1 and HM2 on page 19.

If you search about it you will find https://www.youtube.com/watch?v=oR_RAp73ra0 She also talked about trans-athletes https://www.youtube.com/watch?v=cZ9YAFYIBOU

I have never watch it, and not planning to, so I cannot help you summarize it. Nor have I claimed that she is transphobe, so I don’t feel the need to justify that stand.

If you choose to ignore everything else and focus on this one issue, then I have to admit I don’t know much about it.

I am more and more tempted to donate to EFF every single day.

She has growingly appeal to right wing / corporate rhetorics to attract viewers:

• https://www.reddit.com/r/AskPhysics/comments/1isje08/what_is_the_general_consensus_of_physicists_on/
• https://timothynguyen.org/2025/08/21/physics-grifters-eric-weinstein-sabine-hossenfelder-and-a-crisis-of-credibility/

One of her more controversial take is that academia failed because it is “communism”, and we should privatize science to let corperate and youtube viewers to decide who to fund instead of expert commitees: https://www.youtube.com/watch?v=htb_n7ok9AU

LLM is very good at programming when there are huge number of guardrails against them. For example, exploit testing is a great usecase because getting a shell is getting a shell.

They kind of acts as a smarter version of infinite monkey that can try and iterate much more efficiently than human does.

On the other hand, in tasks that requires creativity, architecture, and projects without guard rail, they tend to do a terrible job, and often yielding solution that is more convoluted than it needs to be or just plain old incorrect.

I find it is yet another replacement for “pure labor”, where the most unintelligent part of programming, i.e. writing the code, is automated away. While I will still write code from scratch when I am trying to learn, I likely will be able automate some code writing, if I know exactly how to implement it in my head, and I also have access to plenty of testing to gaurentee correctness.

https://mastodon.world/@Mer__edith/111563865413484025

I think on android, signal do not use Google’s push notification. They simple send a dummy push, and the signal app wakes up to retrive the latest message directly from signal server.

So Google never have your notification content. I am not sure if they do the same on iOS.

That being said if your attack model includes people reading your notification lock screen, then you should disable showing signal notification.

Usually, I spend $40 in a buffet, annihilate all their snowcrabs, then spend an hour next day on to toilet until my leg is so numb that I can barely stand.

Do I care? No, because I have made it: I make more than minimum wage now.

Codeberg allows private repos: https://docs.codeberg.org/getting-started/first-repository/