Ah gotcha, you could just omit but in this case and the sentence would have the intended meaning.

Why the but? GPL 3 is the correct license to use for open source projects to ensure they stay open and corps don’t freeload on them.

And that’s a very good thing too.

I mean, you could set up your own VPN on a VPS and ensure it doesn’t keep logs. You could also get a VPS in a different legal jurisdiction from where you’re at.

You’r right that only OCaml and Haskell can be used as extraction target for Coq programs. However, it is possible to use Coq to write verified C software. On example is the Verified Software Toolchain that lets you translate C programs to a format that Coq understands and can prove theorems regarding their behavior.

there have been attempts at writing kernels using stuff like Coq https://www.cs.columbia.edu/~rgu/publications/cacm19-gu.pdf

yeah that’s a good overview of different protocols/messengers

My reply from the other thread. People who claim this isn’t true aren’t being honest. The phone number is the key metadata. Meanwhile, nobody outside the people who are actually operating the server knows what it’s doing and what data it retains. Faith based approach to privacy is fundamentally wrong. Any data that the protocol leaks has to be assumed to be available to adversaries.

Furthermore, companies can’t disclose if they are sharing data under warrant. This is why the whole concept of warrant canary exists. Last I checked Signal does not have one.

https://en.wikipedia.org/wiki/Warrant_canary

Yeah, Signal is more than encrypted messaging it’s a metadata harvesting platform. It collects phone numbers of its users, which can be used to identify people making it a data collection tool that resides on a central server in the US. By cross-referencing these identities with data from other companies like Google or Meta, the government can create a comprehensive picture of people’s connections and affiliations.

This allows identifying people of interest and building detailed graphs of their relationships. Signal may seem like an innocuous messaging app on the surface, but it cold easily play a crucial role in government data collection efforts.

Also worth of note that it was originally funded by CIA cutout Open Technology Fund, part of Radio Free Asia. Its Chairwoman is Katherine Maher, who worked for NDI/NED: regime-change groups, and a member of Atlantic Council, WEF, US State Department Foreign Affairs Policy Board etc.