I want to pose another question. I truly don't know the "right" answer!
When we started the BitC work, we were strongly focused on verification. This led to a bias: given that we were dealing with stateful codes, we nonetheless wanted to "exploit" the capacity for pure sub-programs as a way to reduce the analysis load. Eventually, we came to the conclusion that verification has bounded utility, and that for broad purposes type-safety is more important than verifiability. At the moment, the problem of mixing pure and stateful sub-programs is standing out as a deep problem. I find that I am caught between conflicting goals: 1. Get an ([artial) advance in the state of the art/practice into the field. 2. Solve the big problem. Of the two, my personal bias is in favor of [1]. So here is a (value laden) way of stating the question: If BitC, in it's v1 form, gave up on "pure" programming, but leaves the door open to integration of pure [sub]programming in v2, how many of you would no longer be interested? I personally believe that there is real value in a stateful, strongly-typed programming language with high performance. It's considerably less than I initially sought. While I believe the dichotomies can be solved, time is money, and I'm trying to prioritize attention. Not sure what to do, and looking for input and thoughts.... shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
