Stream: Coq users

Topic: Formally verified HTTP requests


view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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: Jan 27 2023 at 00:03 UTC