>We need as many checks as possible - and ideally ones that come for free (e.g., guaranteed by types, lifetimes, etc.) - which is why Rust might be the language for vibe coding.

Checking preconditions and postconditions is much easier to do for a human than checking an implementation

The thing that would really make sense is a proved language like Coq or Promela

You can then really just leave the implementation to the AI.