Moonad is a graphical user-interface and operating system using FM-Net as its assembly, Formality as its native programming language (like C is for Windows) allowing the system to be entirely bug-free, it will use IPFS for storage allowing you to access your desktop from any computer, making the concept of "local storage" obsolete, Unilog for decentralized online applications, replacing the internet entirely (centralized applications could still be emulated as smart-contracts with proprietary keys). It will have a DApp Store, a way to post bounties for programs specified throug Formality types (Provit), mathematical papers will be published as literal Formality, sites will use universal logins so that you don't need to send your passwords in plain text to login on every site/app you access, browsers integrated with crypto so you can pay things with crypto rather than sending your credit card credentials, cute kittens and puppies and anything else you want it to have. It will be great, it is the future, you'll like it and you know that. I'm just tired John, I just want to work on those Agda proofs now, can you continue from now? pls