spectrums_coherence

And fuzzing and static analyzers.

Oh yeah, I don’t play game on it, we only watches YouTube and movies.

So GSConnect actually is a way better experience than any controller in my use case :)

I have a home theater PC and I was really interested in making it have a “TV interface”, but it turns out just the standard dash to dock (on the left), gsconnect, with big scaling and big icons works just fine, if not better :)

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”.

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

I think he has repo pre ChatGPT with legitimate usecases, while that would not be a conclusive proof, I cannot imagine some chatbot would bother with this.

This dude need to chill, he also pushed the systemd change, and in his blog he seems to believe android “advance flow” for sideloading protects users.

The one they are targeting is California’s AB-1043, which still have three quarters of a year before it comes into effect…

I think this dude might get too excited for his new subscription of claude code or whatever, and decided to spam every project with these request. Some of these are reasonable, some are compliance in advance.

Also this dude writes two freaking blog every week with LLM. If I were him, I would try to find some joy in my personal life…