And yet if you announced to a general audience of programmers that you had a marvellous new programming language that guarantees performance but doesn't guarantee correctness, you'd be laughed out of the room.
More seriously, general programming always prefers performance over correctness, because correctnes is expensive and very few programs are rocket surgery where perfect correctness matters. We have languages decdicated to correctnes, like Ada and Coq. They are very niche because they are slow and they require a lot of work the programmer doesn't want to do to hold up their end of the bargain.