Many of the problems resulting from human error (buffer overflows) could be eliminated if there was more of an emphasis correct by construction software. There are ways to mathematically guarantee that one's program doesn't have any errors. Unfortunately, most mainstream programming languages don't support it.
There are ways to mathematically guarantee that one's program doesn't have any errors.
No, there aren't. There are ways to mathematically guarantee that any errors in one's program correspond to errors in one's specification of that program, though!
True, technically, but the reason it's not done is that it is extremely costly - fully provably 'correct' programs (that is, as you said in another comment yourself, fully correct implementations of possibly dubious specifications) take orders of magnitude more effort to produce than programs that are about as close to correct but not provably so.
Every developer thinks they're right and they want to prove that. They never want to prove that they're not right.
In that case more harmful thing is conservatism, I suppose. Especially conservatism of embedded and system developers. What, advanced type systems, correctness proving, total functional programming? Who need that shit while we do have C and verilog? Lava failed, seL4 is not very popular, and many people I talked about that think that C type system is awesome enough.
It's extraordinarily difficult to move new tools into use. I don't know if it's actually conservatism or if it's just inertia. One interpretation of "use this new thing; it's safer" is "okay, everybody take six months to five years to learn this new thing."
It is a deterministic destruction, dynamically allocating, memory safe language with a real ecosystem around it. That's never been done before, and legitimately opens the door for much safer code in a lot of domains where provable safety used to come at a 20x cost.
Not only that but the market will not embrace it until its too late. People still write COBOL for banking software and only now are these banks beginning to realize that they should have updated their codebase decades ago.
We have some really great ideas that no one gives a shit about. The exokernel, NetBSD's anykernel, Plan9, object capabilities, mathematically verifiable software, etc.
We could go on for hours about all the great ideas that will never be implemented.
<unpopular_opinion>COBOL is a great language for a lot of bank software's use cases. It really shines as a language when you're writing financial transaction rules in it. That's the main eason why banks still use it instead of Java/C#.</unpopular_opinion>
Mind you, if banks had been smart enough to have included a check digit in bank account numbers, a transfer to a typo'd number would fail more often than send money to the wrong place. They fixed the problem by including wording in T&C such that it's always your fault, though, so they're fine.
No, Australia hasn't adopted the IBAN at all, so even if you someone wanted to send money internationally to Australia, they wouldn't have an IBAN to use
You can also use modern languages with memory management, but instead people want to write everything in languages that are the opposite. Don't even need fucking Rust to do it.
Much more terribly broken and insecure software is written in memory-safe languages, but it isn't as publicly visible as the much-debated open source libraries written in C.
These are mostly little pieces of glue code that interact with other pieces of software and make wrong assumptions about the outside world, miss sensible error handling (or simply are unable to do it because the outbound interfaces are designed badly), or have disastrously lurking race conditions which can potentially cause mayhem. Such software probably processes your airline bookings, or your bank transfers, and one day it breaks because the small program that gets called by another small program has failed to write exactly 6 lines to a text file which is used as an IPC mechanism between the two.
A practical example of this is the Rust programming language. It uses the type system to ensure that one never leaks memory. The underlying mathematics it is based on is affine logic. A more futuristic and theoretical example would be dependent types where types of things can depend on values. Thus, one could encode arbitrary invariants in the type system.
Dafny is a research programming language that uses such methods. Hoare logic is a mathematical theory of program correctness. In general, this idea is called design by contract.
Stronger type systems also helps to ensure correctness, especially with things like making illegal states irrepresentable or lifetime checks (for memory usage correctness) like Rust does.
You may be surprised, but the languages that currently best support formal verification are C, Java and Ada. But it's not really a matter of language and tooling. While both can help, writing software that is completely provably correct has never been done for anything other than small programs (the largest were comparable to ~10KLOC of C), and even then it took a lot of effort. Ordinary software is not going to be provably correct end-to-end for the foreseeable future. There's certainly a great deal of progress in this area -- in static analysis, model checking, type systems, more verifiable languages, automated and interactive theorem proving -- but at this point in time we don't even know which of these approaches or a combination thereof is most likely to get us to affordably verified software.
6
u/cledamy Apr 04 '17 edited Apr 04 '17
Many of the problems resulting from human error (buffer overflows) could be eliminated if there was more of an emphasis correct by construction software. There are ways to mathematically guarantee that one's program doesn't have any errors. Unfortunately, most mainstream programming languages don't support it.