This is a non-extensive lists of amazing things that would be possible if we had a software platform (browser, OS, whatever) built on top of a proofgramming language like Formality instead of usual programming languages.
Textual/PDF-based academic publishing world we live in is shamefully primitive. Because of the way things are done, there is a gap between mathematical discovery and what can be used in practice. It is very laborious to use the results of a paper in real world programs. Example: LRS. The analogy: Papers are textual programs. Abstracts are comments. Theorems are types. Proofs are programs. Citations are imports. Peer reviewing is the type checker. I see a world where every paper is formalized. Where you can "import a paper" in your code.
Specify the code you need in Formality, press a key. First, the computer attempts to write the code for you (Proof Search). If it fails, it attempts to find it in a global repository of code (Foogle); there is a huge chance that what you are trying to do was already done by someone before. If that fails, it outsources your code to a network of human devs that write it and get paid automatically in crypto, because the computer (i.e., a smart contract) can check that it was implemented correctly (up to your specification). In a few minutes your problem is solved. Why write code when you can just describe it?
Programming languages stopped getting faster due to the sequentialism bottleneck. Example: writing an 2D for-loop to draw a image. On Formality, every single expression that can be evaluated in parallel is. You do not need to be a GPU/CUDA/OpenCL expert to use the GPU, just write a normal for-loop like you would on Python and it is parallel already. No other language can do that because only Formality is based in a confluent, parallel model of computation (interaction combinators).
Smart contracts that can't be drained. Package managers that can't be exploited due to malicious dependency. An operating system simply immune to viruses and malwares. And so on. Proofgramming languages give us a new level of software security that is absolutely needed for a world based on crypto currencies and smart contracts.