Proofs are arguably still better than tests at evaluating efficiency, at least for smaller components/algorithms in isolation. While there are cases where constant factors that can't be described well in a proof matter, in most cases, the crucial element of an algorithm's efficiency lies in how the complexity scales, which can be proven in the vast majority of cases. On the other hand, relying solely on benchmarking introduces a lot of noise that can be difficult to sort through.
If only there was a clear answer to this. Software engineering, as it has appeared to me, has always seemed to evolve with opinions moreso than tangible improvements. That being said, some practices are almost universally agreed to lead to better code, like defensive programming (proving your assertions relating to program conditions in the actual code), uniform documentation, and, in general, taking your time in implementing structures that will be used throughout the codebase. Formalizing your logic in proofs can be one part of that.
Agh, I understand why runes were implemented, but I still can't get myself to like them. It feels like Runes take away from what made Svelte Svelte (the simple, concise syntax), and changes like this seem like slow concessions back in that direction anyway.
QuickJS is great for cases where you are more limited by startup and executable size than anything else but it tends to perform quite terribly (https://bellard.org/quickjs/bench.html) compared to V8 and anything else with JIT compilation.
More code does not inherently mean worse performance.