|| ||"David A. Wheeler" <dwheeler-AT-dwheeler.com>|
|| ||Notice for lwn ("Development" or "Announcements")|
|| ||Tue, 10 Feb 2009 19:12:14 -0500|
Hi - I suggest noting this site in lwn, under "Development" or
Something like this:
A new site, "http://www.openproofs.org/", has been set up to encourage
the development of "open proofs". The site defines "open proofs" as
"software or a system where all of the following are free-libre / open
source software (FLOSS):
* the entire implementation
* automatically-verifiable proof(s) of at least one key property, and
* required tools (for use and modification)"
They've already packaged several FLOSS formal methods tools that can be
used to prove properties of programs and models of programs."
I'm happy to provide more info on it. Basically, "formal methods"
approaches (which let you use math to PROVE things about programs) have
been around for a long time, but the lack of FLOSS examples make it
REALLY hard to make progress in this field. The site hopes to help
--- David A. Wheeler
to post comments)