i've always wondered how web and functional programming interact. there's, for example TypeScript and Elm. These are not designed for mathematical proofs.
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/
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....
https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf