Hello, I am a specialist of a neighbour field so I can try to precise a few things. It's not automated theorem proving they are talking about but more interactive proof or assisted proof. The goal is to write a proof that a computer can check and not to have a computer generating a proof. Most of the time, automatic proofs are just used for small proof steps that would be written as trivial in a pen and paper proof.
This is indeed very important to have a clear semantic, else you can't even write the properties you want to prove. What I don't agree with is that a very precise semantic translate into static type system. A lot of non statically typed languages have a clear semantic too. For example, lambda-calculus have no type at all but a very precise semantic. Having a precise semantic mainly means that the language has been carefully designed and that it is easy to tell, and mathematically formalize, what a program is going to do. Being purely functional is a big help. Having clean concurrent construct with a precise semantic is interesting too. >From this point of view, Clojure has a quite precise semantic. It is probably easier to prove programs in Clojure than programs in C or Java. Even if some people makes a great job in proving Java programs: http://krakatoa.lri.fr/ But proving java programs is harder than proving functional programs whether they are statically typed or not. Proof of imperative programs, when they are not functional programs in hiding - mostly when there can be aliasing - , needs to carry around a full and complete model of the state of memory, whereas pure functions just need to relate arguments and results. And proved programs running java byte code sure is important. Less relevant digression about static typing and Dependant Type Theory ------------------------------------------------------------------------- Now that I have started talking about program certification it is impossible to stop me. So please forgive me if I am too long. The part of this area I know best, Type Theory, proves the correctness of programs by representing properties in very precise types. Types are allowed to depend on values, and computations are allowed to happen in types, making them far more powerful than types in a language than Haskell. Translating these programs to another language (a process called extraction) is not always possible to a usual ML-like language - without unsafe cast - because some expressions are not typable in such a language. There is a few practical examples (including things that look a bit like ClojureSQL) of that in (it's time for self advertisement): http://sneezy.cs.nott.ac.uk/~npo/PowerPi.pdf So being a dynamically typed functional language with clean construct for concurrency makes Clojure an interesting language for certification I believe. Apologies for my long mail, never gives the opportunity to someone to talk about his work... Best regards, Nicolas. > What they are talking about is (semi) automated theorem proving [1] > (subfield of automated reasoning). To do that you need to have a > modeling language with very strict semantics, because you can only > prove if you can 'reason' (make a guarantee based on certain > assumptions) in an way about what a 'sentence' of your model language > says. Very strict semantics with possibility to reason about it > without actually running the program translates in the field of > computer programming languages to static type systems. And here be > sure to notice that the Haskell (static) type system is a couple of > orders of magnitude more capable than the (static) type system of > Java. > > I don't know where you would want to use Java and/or Clojure, but I > doubt that you can get very far, because Java's static type system is > too limited, and Clojure is dynamically typed. I think a functional > language is easier to reason about compared to an object oriented one > (please someone comment on this), but it's not enough for theorem > proving. > > The documentation available in HTML on the site is a bit thin as to > how they actually used Haskell and C together, check the paper: "seL4: > Formal verification of an OS kernel" [2]. The actual implementation > and what they prove (and not prove) can be found in section 2 - > Overview. > > Cheers, > Daniel > > [1] http://en.wikipedia.org/wiki/Automated_theorem_proving > [2] http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.pdf > > > 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. 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. > > > > 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 (high level, some technical background > > assumed) > > > > Statistics (sizes, numbers, lines of code) > > > > Questions and answers (high-level, some technical background assumed) > > > > Verification approach (for technical audience) > > > > Scientific publications (for experts) > > > > Acknowledgements and team > > > > What does a formal proof look like? [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 -~----------~----~----~----~------~----~------~--~---
