[bitc-dev] on mutable types

[Sam Mason]

Hi,

It's probably a bit late for this, but I'm a bit confused by the "mutable"
keyword.  It appears to do two things, firstly it allows the contents
of a variable to be changed at runtime.  Secondly, in providing this
mutability an extra level of indirection is introduced -- it is this that
surprises me.  I would expect it function more like the complement of the
"const" keyword in C.

I assume there are good reasons for this, but it just seems like too
much to me.  My guess is that it makes proving the correctness of
code easier but, having never had to do this before, I'm not sure how.
If it only flagged a variable as mutable then it would mean that proofs
of (mutable (ref 't)) would be equivalent to the current (mutable 't).
Conversely (mutable 't) where 't is not a "ref" type would just be more
difficult to prove the correctness of.

If I did have a C library that accepted a double[] as a parameter, what
would it's type be in BitC?


  Sam