[andai]

It's interesting that mathematics, which is mostly recreational (I received profound disdain at the math department for asking about applications!) has such rigorous standards, but software, which entire civilizations now run on, does not.

[radokirov]

It is because you can precisely define what would make the whole mathematical endeavor collapse (not following the rules of logic or showing inconsistency), while even defining precisely what would be undesirable for software requires bringing in the whole physical world. If you can't define the outcome you want, you can't have rigorous standards to follow.

[pclmulqdq]

If a piece of software is in safety-critical applications these days, it is often required to have a proof of correctness.

[andai]

Like Linux? ;)

[pclmulqdq]

I think you might be surprised that Linux is generally not involved in safety-critical systems. There is a whole separate ecosystem for those applications.

[andai]

What do they use for that? BSD?

[pclmulqdq]

The ones that use an OS generally use seL4 these days.

[andai]

Thanks. "OS considered harmful" is a satisfying answer, too!