I’m still trying to understand what it means for a program to “prove” something. I think about Bruno Iksil, Fabrice Touré, Nick Leeson, where famously (recently) billions of dollars were risk managed in excel.

I noticed on hackage that text.csv doesn’t port to excel (the most usable calculation tool).

Is it possible that if an excel clone were written in one of the proof theoretic languages, accounting shenanigans would be harder to pull off?

TIA

This isn’t really a Racket question, but I hope it’s okay to take a stab at it here.

If a value has a type, that says something about the value. A type like “integer” is fairly common in programming languages, but “even integer” is not at all common. Imagine a type system that is powerful enough to say “even integer” and enforce it. Coq and Agda have type systems powerful enough to express constraints in higher-order predicate logic. But the cost is that developing code that typechecks is more complicated, and is usually done interactively (rather than writing the whole program and submitting it to the typechecker afterwards).

The technology is still under development and not quite practical. But I don’t think this will rule out many shenanigans. The hope is to rule out larger and larger classes of errors, but even if a program is proved correct, one might be able to work within the specification and do something the designer had not anticipated, or simply do something that the formal system doesn’t cover (e.g. “side-channel attacks”).