It’s possible to write flaw-free software, so why don’t we?

Because most people can barely work with basic algebraic expressions let alone formal logical systems capable of expressing correctness guarantees.