[FOM] Project announcement

Andrej Bauer andrej.bauer at andrej.com
Wed May 13 05:04:16 EDT 2009

Dear Sebastian,

how is your project related to other projects with similar goals, for
example Coq, HOL, Isabelle, Mizar, etc? For example, what's different
about correctness of programs in your system vs., say, Coq?


On Tue, May 12, 2009 at 3:06 AM, Sebastian Reichelt <SebastianR at gmx.de> wrote:
> Dear FOM readers,
> I would like to announce a personal project I have been working on for the last few months. It originated as an idea for a software proof verifier, which I've actually started developing now. The primary focus lies on usability, and, closely related, readability of definitions, theorems, proofs, etc. To achieve this, the system employs higher-level concepts than those found in predicate logic. Please visit the project web site, http://hlm.sourceforge.net/, for more information.
> However, the main reason I am posting this here is that the project also has a foundational side: If software-related aspects are abstracted away, the entire formal system can be regarded as an alternative to predicate logic and axiomatic set theory, instead of an abstraction built on top. This system has some unique and (IMHO) desirable properties, which you can read more about at http://hlm.sourceforge.net/semantics.pdf.
> Any kind of feedback would be greatly appreciated. Also, please ask me if something is unclear; I know that my writeup does not quite match the usual standard in mathematics. Thanks to Martin Davis for letting me post this here.
> Regards,
> Sebastian Reichelt
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

More information about the FOM mailing list