Arc Forumnew | comments | leaders | submitlogin
2 points by rocketnia 4248 days ago | link | parent

Quote battle!

"The programmers did not handle the exception because the assumption was made that the program was correct until proved at fault, apparently a feature of the programming culture for this system, (this observation is worth an article in itself)."

Unit tests and type checkers are both part of this culture. They prove a program is at fault, and if the program passes, they have nothing further to say.

What's missing is mathematical proof and, for the remaining informal properties, unbiased empirical testing (including empirical testing of the proof checker).

The best way I know to integrate mathematical proof throughout a codebase is total functional programming with dependent typing. Unfortunately, precise dependent types are notable for being inhibitive to code reuse. (But don't take my word for it; I'm just passing along rumor here, lol.)

A straightforward approach to bring reusability to mathematics would be to study the possible faithful translations from one mathematical discipline to another. This field of study already exists: It's category theory.

I don't have any recommendations for empirical testing. :)