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.