spectrums_coherence

Is the same effect achievable by a local program in user space/container confinement?

I certainly cannot inspect every program I have to run. In fact, most of the modern program have a deep supply chain, and I cannot make sure that there is no point on the supply chain that want to get root :(

I am sorry but the very picture about wondering whether things are AI or not looks terribly like AI…

I am not happy about the license change for the rewrite. Theoretically, affine type system can be used to reason about deadlock and race conditions (although with caveats https://dl.acm.org/doi/abs/10.1145/3571229).

That being said, race conditions are logical bugs, and a programming language is only as powerful as the specification provided to it. It is possible there are condition that developers are simply not aware of.

It seems like specifying the race behavior of coreutil in an language agnostic way would be a fruitful endeavor.

the cryptography module has unit tests and formal verification.

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.

There are three possiblities here: (1) the formal proof community has advanced so much without me knowing (2) your AI produced complete garbage (3) your AI made ground breaking advancements in formal method. 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 fstar/Impl.Signal.Core.fst.hints 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?

You have also claimed there is support for Rocq, Lean, and F*, and the code is here https://github.com/positive-intentions/signal-protocol/tree/staging/signal-protocol-core/proofs

I looked into the Rocq and Lean part of the proof, and there is no proof, all the “correctness” claims are all declared as axioms, which are not proven.

So far, I have sit down and read your code, and I feel it is either a major breakthrough or a complete waste of my time (I am unfortunately leaning towards the latter). I would be furious if my student or colleagues handed me a work of this quality, and I imagine all the experts reading your code will likely feel the same.

I am not angry because your work involves LLM (I don’t like that, but I won’t be angry about it), but because you disrespected my time and effort to review your code by presenting a work that is far from your claim. In turn, I also cannot provide you constructive and technical feedback to you, as the technical part of your project seems hollow to me. IMO, disrespecting the time of your peer is a very good reason to ban people from their community.

Academia is currently being flooded with AI, many are used by compotent individuals so AI is able to hide error in obscure process. For the first time, academia need to deal with a large amount of submission are not in good faith, and that is frustrating for us volunteering reviewers. Your reader, who are also volunteering their time to help you improve, will likely feel the same.

AI is just a tool, that is, you will get as much expertise out of it as you put into it. Like a computer, it will make producing work easier and faster, but it cannot help you build anything you do not understand yourself.

I am glad you are interested in crypto and verification. But to make meaningful contribution will take honest effort as opposed to just prompting a couple so called artificial “intelligence”.

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.

The article says the document is not send to a third party, most likely it uses info on the passport (NFC, not photo) to generate a proof that the holder is an adult.

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

They do need to pay developers to get high quality software, which is especially for a message app centered around security.

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.