Re: Reiserfs 4

[Christian Stroetmann <stroetmann@ontolab.com>]

On the 22nd of July 2014 15:48, Daniel Horne wrote::
>> I promised not to sent any messages to this maling-list anymore, but 
>> this is an exception because the work of my company and me is 
>> directly addressed in a way that might mislead members of this 
>> mailing-list and the broader public and also might have been an 
>> attack on our reputation.
>
> It wasn't intended as such - I'm new to the field of formal 
> verification and wasn't aware of this work.
>
> Thanks for the information, though. I'll read through those links.
>
> -- 
> DH
>

I do apologize for any harsh statement.

To the subject of formal verification:
This is a highly complex task and if it makes sense to formally verify 
R4 has to be approached from several sides:
1. Is R4 in a state that it is matured enough?
2. File systems for general use are a little bit different than the L4 
microkernel, so the complexity that has to be verified might be higher.
3. Is the environment verified as well, for example the operating system 
kernel of Linux?

Actually, I do not know if it makes sense to do it, but if you attempt 
it, then I will have a look on your results.



Best regards
Christian Stroetmann