Automating Formal Proofs for Reactive Systems
goto.ucsd.edu
goto.ucsd.edu
Have thought for awhile that many systems would benefit from one or more "guard" components for which we have formal proofs that no bad things can happen - e.g. you write an equity trading application in Python, but route all the trades through a checker that ensures you aren't trading too much or too often [1].
[1] See Knight Capital 2012, http://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stock...
I think the problem with a lot of ideas around making a "safe" algorithm for money matters, is that you basically just wind up defining the game that your "opponents" will now be playing against. That is, if you have your rules in the open, but they don't, then they are the ones controlling the game.
Consider, it is relatively easy to make money off of a casino. They just don't let you use the strategies that work. Which is fine if you can just boot off actors that you think aren't "playing well." Not so easy otherwise.
2) Reflex does not use testing to verify a user's code. Instead, Reflex automatically produces fully machine checkable proofs that user-provided code satisfies user-provided specifications. Machine checkable proofs (in a proof assistant) provide the strongest possible guarantee about one's code.