Seriously, whatever happened to sanity checks on input?
An exaggeration, but not a very large one. The stock market is a high-speed game, and a lot of players are willing to cut safety features for raw performance.
(Disclaimer: I do not work with any algorithmic trading systems. Humans do a pretty good job of trading, too.)
Jane Street Capital is a good example of a company that advertises their interest in writing good software: http://www.janestcapital.com/technology/ocaml.php
When algorithmic trading software gets written in Agda then your comment might make more sense.
After a few years in banking, I have learned the following phrase applies well here: Mistakes were made.