[FOM] Project announcement

[Andrej Bauer]

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?

Andrej

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
>