> "horribly broken or decades behind the current state of the art"

This is just about vibe-coded programs in general when the approach assumed by the article is taken. For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).

> I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax.

That's more or less what SPARK (and others) do, although specifications for large programs can become nasty.