Shower idea

Implement a web browser using a language that supports dependant types in order to prove its correctness and that no vulnerabilities exist for it.

>>2
Types are propositions and programs are the proofs of said propositions.

>>3

not possible, P = NP

wut