Jonathan S. Shapiro wrote:
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.
I would not agree that value whould be zero considering that writing
coyotos kernel is planned to be done in bitc. For example hardware
interrupts our outside of bitc prover control. Any IO and giving control
back to user mode process are also out of BitC control.
AFAIR it was planned to describe such effects by assertions in direct
form and by some code that "emulates" the behaviour. In some old post, a
some kind of do-not-emit flag for functions has been planned (because
of that post, I used word underspecified rather than unspecified). So
there might be a proof that some property is true provided that some
assertion is true. This implies that the assertions are checked
independently using out of bitc means.
Was this idea abadoned?
Constantine
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
