Caml trading
ocaml.janestreet.com
ocaml.janestreet.com
Besides – why write more code to check if your original code is correct, when you can just write correct code? And if you write software to check your software, then do you have to write software to check the checking software? Police police police police...
Right. That's why you should have software monitoring things instead of a human.
>Besides – why write more code to check if your original code is correct, when you can just write correct code? And if you write software to check your software, then do you have to write software to check the checking software? Police police police police...
Same reason it makes sense to have proof checking software like Metamath. It's fairly easy to write software that has an 90% probability of being correct. It's maybe three times harder to write software that has a 99% probability of being correct, so it's cheaper to write 90% likely to be correct software and then another piece of 90% likely to be correct software that checks it. That's what my intuition says.
Anyway, I think monitoring software would be much easier to write than actual trading software.
if bank_account < 0.9 * prev_bank_account: stop_trading()
First of all, they cannot increase the latency of their software; in fact, as is explained in the presentation, they work hard to keep it as low as possible and to continue to lower it. An extra layer which must monitor everything would increase latency.
Secondly, what are the algorithms used for determining sanity for this monitoring software? The same ones used to determine behavior of the original system? Then what is the point of writing the second, monitoring system? If it's different, then one of them is incorrect.
if bank_account < 0.9 * prev_bank_account: stop_trading()
What does this mean? As a demonstration of generalization, you might as well have written "if (should_stop) stop;" and similarly affected the discussion.
It's fairly easy to write software that has an 90% probability of being correct. It's maybe three times harder to write software that has a 99% probability of being correct, so ...
Their software needs to be as close to 100% correct as can be reasoned. The speaker notes that the static type checking in OCaml helps a great deal with both reasoning about specifications (what do I think this should actually do?) and preventing errors. Easy factorization in functional programming style helps break the problems into smaller components with little state, as well.
it's cheaper to write 90% likely to be correct software and then another piece of 90% likely to be correct software that checks it.
Assuming those statements are true and it were possible for two discrete systems to function in that manner, that still leaves you with a large amount of known probability for error.
You should watch the video, I think you will find especially interesting the part where he describes how they were unable to pay enough money to get people to even carefully review certain types of code.
Additionally, I think you may be conflating static checking (which OCaml does) with live monitoring of a working system: Same reason it makes sense to have proof checking software like Metamath.
That is a static check. Metamath does not fork a process and monitor your proof, assuming that were somehow possible.
That's what my intuition says.
Intuition is often correct when dealing with things which are intuitive.
Right. So there is a sweet spot: you want to monitor often enough that you aren't bankrupt in a millisecond, but not so often that your profit becomes 50% of what it could be. I'm not familiar with the algorithms used in trading, but assuming they're complex, the sanity check that I'm proposing would not use a very large portion of your cycles.
>If it's different, then one of them is incorrect.
The presenter spoke of humans shutting off the system when it was causing them to lose a lot of money (in older days when their system was slower?) Presumably the humans were using some algorithm other than the one they implemented to decide whether to shut the system off. Which algorithm is incorrect?
How complicated do you think the algorithm the humans use would be to implement?
>You should watch the video, I think you will find especially interesting the part where he describes how they were unable to pay enough money to get people to even carefully review certain types of code.
I watched the first half. I stopped watching when it became apparent that I would get more out of the video if I knew OCaml, and I plan to learn it at some point.
>That is a static check. Metamath does not fork a process and monitor your proof, assuming that were somehow possible.
I'm talking about the effectiveness of using one system to confirm the correctness of another. For some reason, someone put a lot of hours into Metamath when they could have put the same hours into checking their own proofs. Why do you think they did that?
A final point: He mentioned that their software is in constant need of updating. Every update is an opportunity to introduce a critical error. It seems likely to me that monitoring software would not be in need of constant updating, since the algorithm that the humans use to determine when to turn off the machine probably does not change along with the things he mentioned.