" Eventually, we came to the conclusion that verification has bounded
utility, and that for broad purposes type-safety is more important than
verifiability."
Couldn't agree more.. I would be less likely to use is if it tried to solve
the "big problem"...
I have stated my views on full verification before and believe it is a
negative thing
-it requires a rare skillset
- it means when you want to make changes a very formal step to change
the specification is often needed hence you need the rare skill set also for
maintenance.
- It is a LOT of work for very little gain eg mainly useful for projects
with very deep pockets
To date the work i have seen on verification of micro kernels are not
impressive , huge amounts of work for a very small part of the code which
has very few bugs anyway ( and the majority of bugs found are resolved with
type safety and buffer overrun checking) . And the cost of making change/
maintenance difficult is IMHO very high. The fact Linux and Windows kernels
are hard to change has caused a LOT of issues , verification makes it much
worse.
That said i favor light verification with some simple Asserts in code
especially if the compiler handles it eg not a separate verifier.
Anyway back to BitC i almost see it like relativity and quantum mechanics 2
fields that are very different and difficult to resolve and the big problem
is akin to unifying them. Bitc is making the correct step in introducing
mutability and static data to what is really a functional language to
extend it to systems and high performance lib programming however there
will be much practical lessons to come out that will become apparent when
writing the standard lib and with larger 50K + line projects.
For me the big things from BitC are
- Can work without GC / non boxed types
- Non null-able types
- Type safety
- Optional Memory safety
- Type classes for light polymorphism
- Functional language support
- Mutable data support.
- Deal with unusual types ( eg cast a index to a byte array to a
variable size message - i do this at the moment with an external C function
...)
And that is it , i don't need anymore until i see what happens in a
larger project and the soft factors become important ( docs , syntactic
sugar , training , ease of use , tools , quality of standard lib) . If it
grows you invest more as a side project to solve the big issues your not
going to have a big user base after v1 anyway , momentum takes time , so
significant changes can be made.
Ben
On Thu, Jan 20, 2011 at 9:02 PM, Jonathan S. Shapiro <[email protected]>wrote:
> 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
>
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
