Hi Coq users! How can I make formally verified HTTP requests with Coq so I can make a formally verified Matrix bot? Is it possible?

Haven't tried it, but https://github.com/liyishuai/coq-http exists and might help. It won't be quick, but it might be lots of fun!

The cost might depend on what kind of formal verification you have in mind, and on how much Coq experience you already have.

Last updated: Jan 27 2023 at 00:03 UTC