Hey Folks,
Sorry for the radio silence over the past month or so, been a busy summer!
Anyhow, our next meeting will be August 15th, Aaron Mansheim will be giving a presentation that touches on Coq, Haskell and dependent types.
Abstract follows:
Since 1999, incorrect implementations of binary search have been shipped by Sun, IBM, Microsoft, and Peter Bentley (author of Programming Pearls).
Even QuickCheck testing isn't enough. Consider that Intel's FDIV bug only gave wrong answers only one millionth of one percent of the time. That problem cost Intel a half billion dollars.
We will demonstrate using dependent types to construct proofs and Haskell implementations of the correct algorithms. Specifically we will use the Coq proof assistant. In June, Coq became the 2013 recipient of the ACM SIGPLAN Programming Languages Software Award: "Coq is playing an essential role in our transition to a new era of formal assurance in mathematics, semantics, and program verification."
Hope to see you there.
Thanks,
MBL
P.S - Shameless plug: if anyone is looking for a job, we're hiring for a variety of positions (middleware type stuff, iOS, Android, etc). If you'd like to work on some big, cool products, let me know!