Hacker News Reader

Comment by lmkg | Hacker News Reader

High-Frequency Trading. When your margins depend on squeezing every last millisecond of performance to beat the speed of the market itself, you don't have time for an extra conditional branch instruction.

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.

View on HN

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.

If you're closing out a short, 0 is a perfect time to sell.

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

Well we are talking about Accenture here...

Reply on news.ycombinator.com