>I just wonder if our time would be better spent developing tools to formally verify memory safety of existing languages,
The industry can't implement your suggestion because while computer science can formally verify a restricted subset of some C source code, we can't write a generalized tool to scan any C code to prove memory safety.
Consider memory operations of existing language such as C Language with these statements:
char *dst; // value is set anywhere in the program
char *src; // value is set anywhere in the program
size_t sz; // value is set anywhere in the program
// ... bunch of other code that may alter dst/src/sz ...
memcpy(dst, src, sz); // is that memory safe?
Nobody has yet written analysis tools to prove & verify that the memcpy() is "safe" because predicting with perfect accuracy how variables dst, src, sz will get set & change during runtime are variations of the unsolvable Halting Problem:
https://en.wikipedia.org/wiki/Halting_problem
That's why there's still no computer science research paper showing a tool that can scan general C source code to prove that all calls to memcpy(), strcpy(), and any writes to RAM via aliases & pointer dereferencing are "memory safe".
We're hoping for "Sufficiently Smart Compiler"[1] type of tool that can verify C code is safe but the source itself doesn't have enough information embedded in it to prove that.
So the alternatives so far have been:
- static approach: extra syntax for manual annotation (C++ unique_ptr<>, or Rust borrow &ersand, or manual mutex lock/unlock)
- dynamic approach: runtime tests with extra memory checks such as Valgrind + UBSAN + ASAN + debugger memory fences, etc. This can catch some but not all memory errors. 100% provable is not possible for non-trivial programs because of the combinatorial explosion of runtime execution paths and memory values.
- GC garbage collection in a different "managed" language. The tradeoff is higher RAM footprint, extra cpu and GC pauses for tracing scanners.
> GC garbage collection in a different "managed" language. The tradeoff is higher RAM footprint, extra cpu and GC pauses for tracing scanners
It would hardly mean a problem for most programs, including OS kernels, especially that kernels are themselves GCs for resources like processes, file handlers, etc.
Also, GC pauses are overblown, most of the tasks can be done in parallel.
The industry can't implement your suggestion because while computer science can formally verify a restricted subset of some C source code, we can't write a generalized tool to scan any C code to prove memory safety.
Consider memory operations of existing language such as C Language with these statements:
Nobody has yet written analysis tools to prove & verify that the memcpy() is "safe" because predicting with perfect accuracy how variables dst, src, sz will get set & change during runtime are variations of the unsolvable Halting Problem: https://en.wikipedia.org/wiki/Halting_problemThat's why there's still no computer science research paper showing a tool that can scan general C source code to prove that all calls to memcpy(), strcpy(), and any writes to RAM via aliases & pointer dereferencing are "memory safe".
We're hoping for "Sufficiently Smart Compiler"[1] type of tool that can verify C code is safe but the source itself doesn't have enough information embedded in it to prove that.
So the alternatives so far have been:
- static approach: extra syntax for manual annotation (C++ unique_ptr<>, or Rust borrow &ersand, or manual mutex lock/unlock)
- dynamic approach: runtime tests with extra memory checks such as Valgrind + UBSAN + ASAN + debugger memory fences, etc. This can catch some but not all memory errors. 100% provable is not possible for non-trivial programs because of the combinatorial explosion of runtime execution paths and memory values.
- GC garbage collection in a different "managed" language. The tradeoff is higher RAM footprint, extra cpu and GC pauses for tracing scanners.
[1] http://wiki.c2.com/?SufficientlySmartCompiler