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.
-
-
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".
-
It's easy to characterize what you call "verification in the small" as properties that can be readily expressed as what's called inductive properties (also, compositional properties). It is also easy to show that most interesting program properties do not have this quality.
- 4 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.