4 ms·

The L4 microkernel was verified that it faithfully implemented the system specification. The system specification is written in (executable) Haskell. http://e

by gvb 14y ago

The L4 microkernel was verified that it faithfully implemented the system specification. The system specification is written in (executable) Haskell. http://en.wikipedia.org/wiki/L4_microkernel_family#Current_research_and_development http://en.wikipedia.org/wiki/L4_microkernel_family#Current_r... So, how do they know the Haskell specification is correct??? I guess it's turtles all the way down. http://en.wikipedia.org/wiki/Turtles_all_the_way_down http://en.wikipedia.org/wiki/Turtles_all_the_way_down

sanxiyn 14y ago
Well, they don't know whether specification is correct, but verification, while proving correctness, also proved (because you need these to prove correctness) no buffer overflow, no null pointer dereference, no unintentional integer overflow, etc. So it's not useless.
- gvb 14y ago
  I agree that is is not useless, however its usefulness is limited to the implementation level, verifying the translation from the Haskell specification to assembly/C/blub implementation is correct. The higher level question is whether the Haskell specification fully and correctly specifies the desired behavior. In my 30-odd years of experience in Mil/Aerospace, I have never seen a fully and correctly specified set of requirements that could be transliterated into correct executable code. If nothing else, they all have had implicit assumptions. That is the Achilles heel of the IBM "Master Programmer" method, reborn as "outsourcing". Since the specification is executable Haskell, that implies they wrote Haskell test programs to show that the specification implements the desired behavior. Writing a program to verify the specification that another program implements... and then claiming a formal proof of correctness of the system is now recursive. Turtles all the way down.
  - sanxiyn 14y ago
    I am quite aware of the problem of specification. For others: I learned a lot from reading the book "Mechanizing Proof". No knowledge of formal methods is needed (but you will learn something about formal methods while reading). I can't recommend the book highly enough. http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Technology/dp/0262632950 http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Tec...

by gvb 14y ago

sanxiyn 14y ago

Well, they don't know whether specification is correct, but verification, while proving correctness, also proved (because you need these to prove correctness) no buffer overflow, no null pointer dereference, no unintentional integer overflow, etc. So it's not useless.

gvb 14y ago
I agree that is is not useless, however its usefulness is limited to the implementation level, verifying the translation from the Haskell specification to assembly/C/blub implementation is correct. The higher level question is whether the Haskell specification fully and correctly specifies the desired behavior. In my 30-odd years of experience in Mil/Aerospace, I have never seen a fully and correctly specified set of requirements that could be transliterated into correct executable code. If nothing else, they all have had implicit assumptions. That is the Achilles heel of the IBM "Master Programmer" method, reborn as "outsourcing". Since the specification is executable Haskell, that implies they wrote Haskell test programs to show that the specification implements the desired behavior. Writing a program to verify the specification that another program implements... and then claiming a formal proof of correctness of the system is now recursive. Turtles all the way down.
- sanxiyn 14y ago
  I am quite aware of the problem of specification. For others: I learned a lot from reading the book "Mechanizing Proof". No knowledge of formal methods is needed (but you will learn something about formal methods while reading). I can't recommend the book highly enough. http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Technology/dp/0262632950 http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Tec...