Re: [seL4] Haskell error comments

Glad to clear that up. Thanks to Tom for raising that point: C "assert" is indeed stripped in the preprocessing phase for the production kernel, but "halt" isn't. It's the design-level (Haskell) assertions we prove don't fail. Cheers, Gerwin

On 28.01.2015, at 2:29 pm, David Greve wrote:

On Tue, Jan 27, 2015 at 5:43 PM, Thomas Sewell wrote:

...

There's a bit of history.

There always is ..

...

We did discover once, after verification, that one of the C assertions was wrongly transcribed from its Haskell counterpart, so the debug build of the kernel could panic in a situation where nothing was actually wrong.

That is an interesting story.

...

Well, that's probably more details than you ever wanted to know.

Actually, this is precisely why I asked.

Thanks, Dave

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.