Show HN: i2forge – A Platform for Verified Reasoning

Welcome to the i2forge demo. We are building a platform that makes formal verification easy.

The box beneath accepts i2 code and verifies that provided proofs are correct. It's a bit finicky, but you should be able to prove some simple theorems in it. Hit "Verify" to see how it handles the example input, and then put in your own.

/* eq: Equality. i2 currently supports only logical operators and funtional * application, because we haven't yet found a simple way of introducing * higher-order operators (such as the equals-sign). */ @func eq(x any, y any) bool; /* nat: A natural number. */ @func nat(x any) bool; /* 1 is a natural number. */ term 1 nat; /* This is like a global constant declaration. It occupies the place of Peano's * first axiom that 1 ∈ N. */ /* succ: For each x there exists exactly one natural number, called the * successor of x. */ @func succ(x nat) nat; /* injectivity: If succ(x) == succ(y) then x == y. */ @tmpl injectivity(x nat, y nat) { eq(succ(x), succ(y)) ==> eq(x, y) }; tmpl thm1(m nat, n nat) { !eq(m, n) ==> !eq(succ(m), succ(n)) } { eq(succ(m), succ(n)) ==> { injectivity(m, n) } eq(m, n); };

i2's output is currently very raw, as we are trying to determine exactly what it should output. The last line, however, should be self-explanatory. When i2 outputs "qed" it means it has verified the theorem it was considering.

At first glance, the block above is certainly difficult to understand. If you'd like to understand this better, we will be posting a tutorial shortly, so you can watch this space.

What is i2forge?

As we mentioned above, i2forge is a platform we are building with the express purpose of reducing the up-front investment that mathematicians must make to use formal verification. We want to make formal verification accessible and fun to the average mathematician. i2forge is based on the i2 language, a novel take on formal verification that we will be working on as an open source project.

How far along are you?

Extremely early stages. We began studying to build i2 late last year, and wrote the first lines of code in February. The first end-to-end success (verifying a file very similar to the one given above) was a couple of weeks ago.

That being said, we are very encouraged by the speed at which i2 and i2forge are becoming usable. This is why we are ready to share our adventure with you.

Who are you?

See here if you would like to get to know us.

How can I use i2 and i2forge?

We are launching a closed alpha for i2forge today, and will be handing out a limited number of invites over the next week or so. Because of the early and unpolished state of the platform, we are most interested in working with mathematicians (and others) who are desperate enough for good FV tooling as to be willing to deal with the inconveniences of an incomplete and buggy system. If you answer to this description, send us a brief email introducing yourself at access@i2forge.com and we will try to give you access as soon as possible.

If your interest is purely in the language, and not in the platform, we have published i2lang as an open source project, and welcome your participation as a user and contributor.

How can I share my thoughts with you?

Talk to us on the i2forge Discord server.

from Hacker News https://ift.tt/UntlPs3