[Haskell-cafe] Formal Methods/Functional programming job position at Intel
Our formal methods team at Intel has a full-time position available that I think would be a good fit for functional programming and formal methods enthusiasts. I'm including the description below. Do not hesitate to contact me if you've any questions, or just want to talk about it in general. To apply for the position, please visit: http://www.intel.com/jobs/jobsearch/index.htm, and in the advanced search area enter the job number: 709631. Thanks, -Levent. Job Description *Formal Methods Validation Architect* *-* *709631* Description If you're interested in products going into future super computer markets then the Intel® Many Integrated Core (Intel® MIC) Hardware Engineering Group is the place for you! We design and validate silicon chips with many Intel cores integrated inside being used in high performance computing architectures. In this position you will work as part of the pre-silicon formal methods, tools, and verification team to support a continued high quality of the future Intel many core processor products. You will work together with Intel's formal verification and validation community, the Formal Verification Center of Expertise (FV CoE) in a team of experts in formal methods and AV Validation. Your specific responsibilities will include defining formal verification (FV) test plans as well as Cluster Test Environment (CTE) based test plans for dynamic simulation validation (DV). The goal is to help optimize a combined use of FV and CTE based validation techniques (DV) and contribute to an increasing use of formal methods at Intel. Based on the test plans you will write properties in formal language, and prove the properties using our model checkers and theorem proving tools. You will also write CTE based test cases and coverage plans. Your area of strength may currently lie within either FV or DV with strong skills rooted in software development. But through your skills and work, you will become an expert in both formal methods and validation technologies. You will interact very closely with design teams, and other validation teams, as well as with Intel's internal RD groups that continue to improve and develop formal method and verification tools. You must be able to communicate effectively with various technical groups and coordinate activities amongst those groups. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] formal methods functional programming
Abigail wrote: Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information. Functional programming in pure functional languages like Haskell can help to make programs easier to reason about - but it doesn't _remove_ the need for formal methods. For example, there are laws about certain classes such as Monad and Monoid which all instances of those classes must follow in order to be considered proper Monads or Monoids. However, in order to reason about functions defined over all Monads (say), we need to know that those laws hold for _all_ possible Monads (without laws, we don't really know anything about the methods of Monad - in a non-strict language, the methods might not even be well-defined for certain inputs). But Haskell doesn't even have a way to _state_ these laws formally, much less _prove_ them! I am working on a functional programming and specification language in my spare time which does have such formal methods features built-in, but it is not even implemented yet. (I can email you if I ever write a paper on it, but it may be some years before that happens.) However, there are various other angles which you can research: 1. Proofs as programs: _Constructive_ proofs of theorems can be automatically converted into programs in a functional programming language - although these programs are not always efficient. Indeed it is possible that a generated program will be far too inefficient to be useful. See for example Proofs, Programs and Executable Specifications in Higher Order Logic, a Phd thesis by S Berghofer at http://www4.in.tum.de/~berghofe/papers/phd.pdf 1a. Models as functional programs: The very first sentence in Chapter 1 of the thesis I just cited, says: Interactive theorem provers are tools which allow [one] to build abstract system models, often in some kind of functional programming language involving datatypes and recursive functions. 2. Dependent types: By programming in a dependently-typed functional programming language such as the research language Epigram, it is possible to write functional programs whose types force them to be correct. See for example Why Dependent Types Matter by Thorsten Altenkirch, Conor McBride, and James McKinna. However, in my opinion this is only useful for simple sized types such as a list of length 6. For more complicated properties, I believe this approach is unnecessarily difficult, and does not match how mathematicians or programmers actually work. My approach (see above) clearly separates the programming, the theorems and the proofs, and (in principle) allows all three to be written in a fairly natural style. As opposed to dependent types which, in Epigram at least, seem to require threading proofs through programs (for some non-trivial proofs). 3. Separate formal methods tools for Haskell: My approach is to integrate formal methods directly into the essential core of a language, but this is quite unusual to say the least - a more normal thing to do (whether for functional or imperative languages) is prepare a separate formal methods tool for an existing programming language. This has been done for Haskell - see Verifying haskell programs using constructive type theory by Abel et. al. at http://portal.acm.org/citation.cfm?id=1088348.1088355 I have not considered testing in this email because another email already mentioned QuickCheck. -- Robin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] formal methods functional programming
Robin Green wrote: 2. Dependent types: By programming in a dependently-typed functional programming language such as the research language Epigram, it is possible to write functional programs whose types force them to be correct. See for example Why Dependent Types Matter by Thorsten Altenkirch, Conor McBride, and James McKinna. However, in my opinion this is only useful for simple sized types such as a list of length 6. For more complicated properties, I believe this approach is unnecessarily difficult, and does not match how mathematicians or programmers actually work. My approach (see above) clearly separates the programming, the theorems and the proofs, and (in principle) allows all three to be written in a fairly natural style. As opposed to dependent types which, in Epigram at least, seem to require threading proofs through programs (for some non-trivial proofs). I would just like to point out that there is nothing that forces you to thread the proofs through the programs. With dependent types you have this option, but you can also write standard Haskell code and have your proofs be separate. It's up to you to choose which way you do things. (If you do separate proofs you can even add some construct to the logic that makes it classical if you like.) Furthermore, I don't see such a clear separation between your points 1 and 2. With dependent types you are making proofs and then using them as programs. How much extraction you do is a matter of optimization, I'd say. And how efficient the extracted program is depends on which proof you choose to do. -- Lennart ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] formal methods functional programming
Lennart Augustsson wrote: Robin Green wrote: 2. Dependent types: By programming in a dependently-typed functional programming language such as the research language Epigram, it is possible to write functional programs whose types force them to be correct. See for example Why Dependent Types Matter by Thorsten Altenkirch, Conor McBride, and James McKinna. However, in my opinion this is only useful for simple sized types such as a list of length 6. For more complicated properties, I believe this approach is unnecessarily difficult, and does not match how mathematicians or programmers actually work. My approach (see above) clearly separates the programming, the theorems and the proofs, and (in principle) allows all three to be written in a fairly natural style. As opposed to dependent types which, in Epigram at least, seem to require threading proofs through programs (for some non-trivial proofs). I would just like to point out that there is nothing that forces you to thread the proofs through the programs. With dependent types you have this option, but you can also write standard Haskell code and have your proofs be separate. But wouldn't that alternate way break the principle, recommended by Cardelli, that all code should be well-typed and the types of all terms should be, shall we say, plainly deducible from the code alone (i.e. not requiring any difficult reasoning on the part of the human reader)? If not, could you give an example to illustrate your point? It's up to you to choose which way you do things. (If you do separate proofs you can even add some construct to the logic that makes it classical if you like.) Furthermore, I don't see such a clear separation between your points 1 and 2. With dependent types you are making proofs and then using them as programs. How much extraction you do is a matter of optimization, I'd say. And how efficient the extracted program is depends on which proof you choose to do. Well I thought someone might say something like that - which is why I called them angles on the question. :) But while statements about types and statements about values might be inter-convertable, I think they look different and one can be more convenient than the other for various purposes. I've only used dependent types trivially so I could be wrong. -- Robin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] formal methods functional programming
I confess I haven't really been following this discussion, but a friend of mine has a recent paper that might be of interest (though it deals with ML rather than Haskell)... http://math.andrej.com/2005/04/09/specifications-via-realizability/ -- Hal Daume III | [EMAIL PROTECTED] Arrest this man, he talks in maths. | www.isi.edu/~hdaume ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] formal methods functional programming
Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information. can u hel me?. Thanks Abigail. __ Correo Yahoo! Espacio para todos tus mensajes, antivirus y antispam ¡gratis! Regístrate ya - http://correo.espanol.yahoo.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] formal methods functional programming
I can't think of any Haskell papers about ``formal methods'' in software engineering, but many papers and books talk about proving program correctness, which is difficult in traditional, imperative languages (which is why it is probably not stressed as much as //testing// is in formal software methods). Paul Hudak, in the textbook, The Haskell School of Expression (http://www.amazon.com/gp/product/0521644089/104-7074974-5852762?v=glancen=283155) writes a lot about proving program correctness (especially induction on recursive algorithms) for Haskell and purely functional programs, reasoning mathematically. If you want to do strenuous testing, you can use QuickCheck: Automatic Specification-Based Testing: http://www.cs.chalmers.se/~rjmh/QuickCheck/ A professor I had at Caltech researches formal methods in constructing reliable software systems, specifically using robust programming language and compiler technology (in this case OCaml). http://mojave.caltech.edu/ Jared. On 1/14/06, Abigail [EMAIL PROTECTED] wrote: Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information. can u hel me?. Thanks Abigail. __ Correo Yahoo! Espacio para todos tus mensajes, antivirus y antispam ¡gratis! Regístrate ya - http://correo.espanol.yahoo.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- [EMAIL PROTECTED] http://www.updike.org/~jared/ reverse )-: ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] formal methods functional programming
Abigail [EMAIL PROTECTED] writes: Hi, I have been searching papers about tha raltionship between formal methods in software engineering and functinal programmming, but i haven't found enough information. I don't think there are any papers, but Galois Connections employs Haskell and formal methods such as proof checkers in our work. You might email for more information: http://www.galois.com/ peace, isaac ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
