Hi everyone,
I just submitted a talk proposal for MOSC 2010 titled "No Bugs, No Holes: Can
Proof Assistants Help Achieve Software Perfection?"
I was wondering if the topic would be of any interest at MOSC so I thought of
asking you guys for some feedback.
The abstract goes: "No one wants bugs in their code, especially not those
exploitable as security loopholes by malicious adversaries. One promising (and
controversial) solution relies on automated mathematics to logically prove that
code not only is free of bugs such as buffer overflows but also meets strict
security and correctness specifications. This talk overviews the history,
controversy, challenges, and success stories of open-source proof assistants
such as Coq and Isabelle/HOL. "
To be honest, open-source tools like Coq are obscure except to a small
group of software developers (who generally don't carry such titles on
their business cards anyway). It's even been argued that they /should/
remain obscure.
I was thinking however, that one way we could carve a (lucrative!) niche
for ourselves is by focusing on high-value-add opportunities such as the
provisioning of high-assurance systems. Roughly speaking, high-assurance
means that if the system fails, someone dies. Such projects by their very
nature require nothing short of generous financial backing.
One way such systems are successfully engineered is via mechanized
formal logic as embodied by so-called proof assistants.
Any comments/questions on the viability of this topic for MOSC?
-- Kim-Ee
--
Join Open Source Developers Club Malaysia http://www.osdc.my/
Facebook Fan page
http://www.facebook.com/group.php?gid=98685301577
http://www.facebook.com/OSDC.my
You received this message because you are subscribed to the Google
Groups "OSDC.my Mailing List" group.
To post to this group, send email to [email protected]
To unsubscribe from this group, send email to
[email protected]
For more options, visit this group at
http://groups.google.com/group/osdcmy-list?hl=en
