What would be ELI5 use case of this? It has been almost a decade since I did anything math-formal in college, and I wonder what would be some practical uses or situations is SW dev where you should turn to this language.

EDIT: I skimmed the intro to Verifiable C, and I think I vaguely understand the idea - do I get it right, that the point is to basically create a formal definition of the function you are writing, i.e if you have a function that takes an array and sorts it, you’d have something like

For every sequence a and every i, 0 <= i < len(F(a)) -> F(a)_i < F(a)_i+1

(Or whatever would the correct formal definition be, I don’t really remember the details, I know I missed some stuff about properly defining the variables, but the idea of the definition should be kind of correct)

And then you define this formal definiton in CoQ, then somehow convert your code into CoQ code it can accept it as F(a), and CoQ will try to proove formally that the function behavior is correct?

So, it’s basically more robust Unit Testing that’s backed by formal math proofs?

I think I know who killed him.

By 11, he was programming on his own—a skill he used to playfully torment his friends. One remembers Balaji’s idea of a middle-school prank: writing code that deleted a friend’s Skyrim save file.

I use Pixel with GrapheneOS as my phone, and I just have a separate profile that only has WhatsApp installed and nothing else. Since the profiles are completely separated, it doesn’t have access to anything else I do on the phone and it’s not running in the background (the profiles are basically sandboxed fresh slates, and switching it can be set-up to behave in a same way as basically turning off the phone as far as the profile is concerned).

When the bridge asks me to log in again or refresh a session, I simply switch to the second profile for a minute and re-log in. I’ve heard iIt might be possible to set up an emulator and leave it running on the server, but that felt like too much effort.

I’ve been using it for almost a year by now, and so far I didn’t have any problems. I’ve not considered that problem though, so it might be happening and I was just lucky.

I’m hodsting my own Matrix server with WhatsApp, Telegram, Discord (you don’t need a bot for that, you can just share your login with the bridge) and Messenger bridge. I have all my IMs in one app, don’t have to install spyware on my phone, and I can make bots that troll annoying people that message me on any platform.

Hosting it was super simple, thanks to the Ansible project that’s extremely robust and well done, I literally just got a hosting, domain amd changed like 5 config values to enable the bridges I wanted, gave it an IP and ssh key, and ran it. And if I need to update, I literally “just update” (it’s all wrapped up into “just” tool), and it eve handles cases where I didn’t update for a while, failing graciously and telling me what I need to do maually, usually just rename some config values.

I wholly recommend it. You probably wont convince your friends to switch from <insert app here>, and this is the best compromise.

I’m using a small instance on Hetzner, for 6$ a month. You could in theory get a free oracle cloud instance for it, but I didn’t manage to get one.

And you can easily share it with anyone interrested, make them an account, so they can also consolidate their DMs. I’m sharing it with a few friends and colleagues.