Incorrect. Have a look at the Swift OpenCombine library. Multiple Publishers of a particular type that emits a single boolean value (e.g., an "Agree to Terms" UI checkmark and an "Agree to Privacy Policy" UI checkmark) are combined at compile-time to be transformed into a single Publisher of a type that emits only a single boolean value (e.g., the enabled/disabled state of a "Submit" button). Effectively, it is not possible to even compile an app that incorrectly ignores one of the "Agree" checkmarks before enabling/disabling the "Submit" button.
> It's next to impossible to type check (...) memory corruption
Incorrect. Have a look at the Rust standard library. Sharing data across multiple treads requires passing a multi-threaded Mutex type; attempting to share data through a single-threaded Rc (reference-counted) type will not compile. Once the Mutex type is passed, each thread can only access the memory the Mutex type represents by acquiring another type, a MutexGuard, through locking. Effectively, it is not possible to even compile a program that incorrectly ignores multi-threading or incorrectly accesses memory in a race condition with other threads thus possibly corrupting that memory. Moreover, it is also not possible for a thread not to properly release a lock once the MutexGuard type goes out of scope.
> All the problems you talk about can be solved with more advanced proof based checkers.
Unlikely. Without feeding strong type information that describes your problem domain into a checker, the checker cannot reason about your code and figure out possible errors. A strong type system is a "language" for a programmer to communicate with his or her checker.
> You say it's paramount to move error detection to compile time. I say, this problem is ALREADY solved, but remains unused because these methods aren't PRACTICAL.
> [the C language] has type checking. Yet people still write unit tests for it. Why? Because type checking is mostly practically inconsequential.
Please do not hold it against me if I do not continue commenting here - you must be from a different, parallel Universe. (How is Elvis doin' on your end? ;) J/K)