[bitc-dev] Representation and memory model
Jonathan S. Shapiro
shap at eros-os.org
Wed Aug 31 14:12:19 EDT 2005
On Thu, 2005-09-01 at 00:57 +0700, Constantine Plotnikov wrote:
> I do not know if there will be the same complication in BitC because
> foreign function interface and its interaction with storage model are
> somewhat underspecified.
Actually, they are not. The semantics of foreign function interface are
very consciously and deliberately excluded from the specification. The
minute you step out to code written in another language, you step
completely outside the BitC semantics, and the utility of BitC as a
language for expressing verifiable code goes to zero. If this is what
you wish to accomplish, use C. C will always be better at being C than
BitC will ever be.
More information about the bitc-dev