> "I prefer to use strong typing and proofs to ensure it does not break at runtime" This has not been my experience with C++ (segfaults etc.) or Java (runtime

> "I prefer to use strong typing and proofs to ensure it does not break at runtime" This has not been my experience with C++ (segfaults etc.) or Java (runtime introspection and exceptions). In ye olde languages compilation seems to be mostly (more than 50%) motivated by performance rather than correctness. Compiled languages have been doing steadily more compile-time work and improving ergonomics lately.