Here's another thing I believe: The next mainstream programming language (or family of them) will have functional-logic underpinnings like backtracking, unification, and failure. The move will be driven by the improvements in writing code that's concise, correct, and verifiable.
Yes, the general case of verification is theorem-proving. The ultimate language ultimately support that, but ought to also make it much easier than present to adopt small-scale verification easily.
-
-
For example, today accessing vertices through an integer index buffer introduces a potential array-out-of-bounds at every step. If we could make those accesses into potential failures, the compiler could point that out for us.
-
Then if we could express that index buffer as an array of natural numbers less than the number of vertices, then the compiler could recognize that and generate safe and faster code. This is the spirit of verification "in the small".
- 5 more replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.