never heard of proof assistant before, how is it different from those
testing tools??
On 15 May 2010, at 16:00, Harisfazillah Jamel
<[email protected]> wrote:
Hi,
Look good in devlopers tracks. Have you submit to
http://conf.oss.my/cfp.html
Thanks.
On Sat, May 15, 2010 at 10:28 AM, <[email protected]> wrote:
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
--
My Facebook
http://www.facebook.com/linuxmalaysia
My Blog
http://blog.harisfazillah.info/
My Network
http://www.facebook.com/pages/Bukan-Sekadar-Internet-Sahaja/100866715422
http://linuxdotmy.multiply.com/
--
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
--
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
