08/12/2017 (Sat) 10:51:28
No need for auditing the software, if you use formal methods along the way. For example, built-in specification constructs, dependent-type language and also techniques like object capability based syntax and capability-based SE.
Logic languages, generally, also have a better safety (see lambda-prolog and Twelf), although they can be limited.
If automated theorem proffers ever became simple enough to use and go mainstream, we could see better software.
But, really, the basis of computing is already "wrong", even on processor level. Maybe the future could be a NISC computer, where there's no separation between firmware, BIOS, payload, bootloader or operating system. It's everything a single compiler, where this compiler apply formal proofing to software running and report errors. Without fixing those errors, your software will not run. This would also allow better sandboxing and better performance.
But I'm not an specialist and don't understand nothing of this, really.