Stream: Coq users

Topic: Formally verified HTTP requests

Github's Fifn2 (Apr 27 2021 at 00:05):

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?

Paolo Giarrusso (Apr 27 2021 at 09:51):

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!

Paolo Giarrusso (Apr 27 2021 at 09:53):

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: Oct 13 2024 at 01:02 UTC