Announcing Copilot 0.22: Can you write a list in Haskell? Then you can write embedded C code using Copilot. Here's a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even numbers: fib :: Streams fib = do "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib") "t" .= even (var "fib") where even :: Spec Word64 -> Spec Bool even w = w `mod` const 2 == const 0 Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin's Atom[1] (thanks Tom!). Copilot was originally developed to write embedded monitors for more complex systems, but it can be used to develop a variety of embedded code. HACKAGE: http://hackage.haskell.org/package/copilot WEBPAGE: http://leepike.github.com/Copilot/ (with more info). PICS/VIDEO of Copilot's maiden flight: http://picasaweb.google.com/105722675808588603973 A PAPER (PDF): http://www.cs.indiana.edu/~lepike/pub_pages/rv2010.html The Copilot Team * Maintainer: Lee Pike (leepike@galois.com), Galois, Inc. * Alwyn Goodloe, National Institute of Aerospace * Robin Morisset, École Normale Supérieure * Sebastian Niller, Technische Universität Ilmenau [1] http://hackage.haskell.org/package/atom