But the big players do the safety checks at compile time, so at runtime, it's simply not possible to make one of these mistakes. Theorem proving might not be necessary for your "hello world" rails app, but it is something that the finance industry likely applies.

(Disclaimer: I do not work with any algorithmic trading systems. Humans do a pretty good job of trading, too.)

I can't tell if you're joking.

There is certainly a culture of micro-optimized C++ in the finance world, but it's not all like that. (It's easier to do easy things than it is to do hard things, and so there is going to be more easy-to-write software in existence than hard-to-write software. Hence why you see so much bad C++ -- it's really easy to write bad C++.)

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

The OCaml type system is a really weak form of theorem proving-- the fanciest usable thing you can do is phantom types.

When algorithmic trading software gets written in Agda then your comment might make more sense.

You can run theorem provers on top of these languages, though.

My guess is that the algorithms do well within say one standard deviation range but beyond that the computers step away. Once the computer volume drops, markets get thin and "Market Orders" produce the results you see. You see bad fills quite a bit in penny stocks but never in these large volume stocks.

hahahahahahahaha sanity checks on input at compile time hahahahahahahaha

I have wonder whether any of that software crashed from divide by zero errors. :-)

I guess somebody forgot to put a check in the software that says that if a share trades at 0 there is no use selling it.

Well we are talking about Accenture here...

Except that to close out a short, you are the buyer, not the seller.