spectrums_coherence

My college does the same, but depends on the professor. Most would sit in the hallway and just chill.

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…

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 :)

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.

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

I don’t think it is terribly expensive, a lot of (somewhat large) domain specific academic instances are maintained by grad students with donation from academics. As far as I know, many of them are in good financial standing.

There are several non-profit had their own instance, like ACM. I recall Mozilla used to do, but I am not sure if they still does.

Then this post should interest you: https://social.growyourown.services/@FediFollows/112419076551165888 :)

And my absolute favorite is @[email protected]

BTW, there is a very strong Boston/Cambridge/Somerville community on mastodon, there is a entire instance for it: https://better.boston/explore

Mayor Wu is on there @[email protected] but not posting much these days.

There are also many people on other instances, like transport or OSS instance, as many prominent OSS contributor lives in that area.

Gnome has parental control https://help.gnome.org/gnome-help/parental-controls.html

But it has some serious limitations: for example, you cannot block individual website reliably. Parents can consider piholes, but DNS sink hole on local network are often trivial to bypass.

Nearing absolute zero even.

I feel if everything they said is true, then this is a reasonable solution. But from my many Youtube scammer video experience, like people have already mentioned, most scammers use standard remote access software, not some bespoke APK.

Why have we been talking about EU chat control for years. How many time have this been voted on? and can people just keep popping up chat control if the previous one fail?