You'd probably do it in the theorem prover extracting it to a language with a web framework or use a language with a web framework that are both easier to prove

You'd probably do it in the theorem prover extracting it to a language with a web framework or use a language with a web framework that are both easier to prove. Here's a few places to explore: http://www.impredicative.com/ur/ http://www.impredicative.com/ur/ https://wiki.haskell.org/Web/Frameworks https://wiki.haskell.org/Web/Frameworks Note: You'd pick the purest of them probably. Most work I've seen on web applications with formal focus used model checkers, though. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397.742 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397.... https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf