Cherry picking only the accurate prediction makes it seem like the predictor is really good!
Look at the rest of that quote:
> The human, computer pair, will also interactively suggest, confirm and fine tune specifications of mathematical properties and invariants at points in the the program.
That hasn't happened and as far as I am aware, is not even close.
> This will help the computer assistant to not only better understand the program but also to to generate real time, verification test runs using SAT technology,
Ditto.
> Interactive testing will eliminate whole classes of logic bugs, making most non ui code correct by construction.
Ditto..
So, 1 out of 4 predictions correct, which makes it worse than random chance?
I don't know, some of that is at least starting to happen with Idris 2, though not in the exact way predicted: https://www.youtube.com/watch?v=mOtKD7ml0NU (Type Driven Development with Idris 2)
Short summary of linked video: when your type system is powerful enough you can restrict the set of possible implementations to the point that the compiler can make a decent guess as to what the program should be to satisfy the type signature.
A flat prior over a probability space with only four possible events, but in reality there are of course many more possible events from which those four were originally picked.
Look at the rest of that quote:
> The human, computer pair, will also interactively suggest, confirm and fine tune specifications of mathematical properties and invariants at points in the the program.
That hasn't happened and as far as I am aware, is not even close.
> This will help the computer assistant to not only better understand the program but also to to generate real time, verification test runs using SAT technology,
Ditto.
> Interactive testing will eliminate whole classes of logic bugs, making most non ui code correct by construction.
Ditto..
So, 1 out of 4 predictions correct, which makes it worse than random chance?