Executive summary: seems like big announcements of "provably correct software" would be easier to achieve in Java+Clojure than for C/Haskell used in the current "big news" regarding a provably secure kernel<http://news.cnet.com/8301-1009_3-10310255-83.html?tag=newsEditorsPicksArea.0>. However, given the bugs I enountered in a java-based DVR contract-from-hell that was a deadlocking side-effecting nightmare<http://reviews.cnet.com/digital-video-recorders-dvrs/directv-hr20-directv-plus/4505-6474_7-32065196.html>, I think this kind of "provability" work would be very useful for real world java and clojure running in "embedded java" whether it be a DVR glitching-out due to an improbable concurrence, or hospital life-support equipment, or aircraft control, military control, etc.
Seems like this could also be a good potential "marketing opportunity" for Clojure, were it to be used as the basis for building provably-correct apps that run in a JVM. I think that market is much bigger than the "provable microkernel in C" market. E.g. toolkit for building probably secure and reliable cell-phone/multimedia java apps, or toolkit for building embedded controller software on which people's lives depend, literally.... http://ertos.nicta.com.au/research/l4.verified/ and http://ertos.nicta.com.au/research/l4.verified/approach.pml > The L4.verified project A Formally Correct Operating System Kernel In current software practice it is widely accepted that software will always have problems and that we will just have to live with the fact that it may crash at the worst possible moment: You might be on a deadline. Or, much scarier, you might be on a plane and there's a problem with the board computer. Now think what we constantly want from software: more features, better performance, cheaper prices. And we want it everywhere: in mobile phones, cars, planes, critical infrastructure, defense systems. What do we get? Mobile phones that can be hacked by SMS. Cars that have more software problems than mechanical ones. Planes where computer problems have lead to serious incidents. Computer viruses spreading through critical infrastructure control systems and defense systems. And we think "See, it happens to everybody." It does not have to be that way. Imagine your company is commissioning a new vending software. Imagine you write down in a contract precisely what the software is supposed to do. And then — it does. Always. And the developers can prove it to you — with an actual mathematical machine-checked proof. Of course, the issue of software security and reliability is bigger than just the software itself and involves more than developers making implementation mistakes. In the contract, you might have said something you didn't mean (if you are in a relationship, you might have come across that problem). Or you might have meant something you didn't say and the proof is therefore based on assumptions that don't apply to your situation. Or you haven't thought of everything you need (ever went shopping?). In these cases, there will still be problems, but at least you know where the problem is not: with the developers. Eliminating the whole issue of implementation mistakes would be a huge step towards more reliable and more secure systems. Sounds like science fiction? The L4.verified project demonstrates that such contracts and proofs can be done for real-world software. Software of limited size, but real and critical. We chose an operating system kernel to demonstrate this: seL4<http://ertos.nicta.com.au/research/sel4/>. It is a small, 3rd generation high-performance microkernel with about 8,700 lines of C code. Such microkernels are the critical core component of modern embedded systems architectures. They are the piece of software that has the most privileged access to hardware and regulates access to that hardware for the rest of the system. If you have a modern smart-phone, your phone might be running a microkernel quite similar to seL4: OKL4 from Open Kernel Labs<http://www.ok-labs.com/> . We prove that seL4 implements its contract: an abstract, mathematical specification of what it is supposed to do. Current status: completed successfully. More information: - What we prove and what we assume<http://ertos.nicta.com.au/research/l4.verified/proof.pml> (high level, some technical background assumed) - Statistics <http://ertos.nicta.com.au/research/l4.verified/numbers.pml> (sizes, numbers, lines of code) - Questions and answers<http://ertos.nicta.com.au/research/l4.verified/faq.pml> (high-level, some technical background assumed) - Verification approach<http://ertos.nicta.com.au/research/l4.verified/approach.pml> (for technical audience) - Scientific publications<http://ertos.nicta.com.au/research/l4.verified/pubs.pml> (for experts) - Acknowledgements and team<http://ertos.nicta.com.au/research/l4.verified/acks.pml> - What does a formal proof look like? [pdf]<http://ertos.nicta.com.au/research/l4.verified/sqrt-2-proof.pdf> Niels http://nielsmayer.com --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en -~----------~----~----~----~------~----~------~--~---
