Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Show HN: i2forge – A Platform for Verified Reasoning

i2forge.com

Post reply on HN
Print view View original

1–10 of 14 posts

Show HN: i2forge – A Platform for Verified Reasoning

#1

Post by akiarie »

Hi! We're Amisi and Claude, builders of the i2 language and the i2forge platform. i2 is an (early draft of a) language designed to make formal verification easy for mathematicians.

We are launching the language as an open source project today (https://i2lang.org) together with a closed alpha for i2forge.

However, we have a publicly accessible demo page which anyone can use, and we would love your feedback.

Thanks.

Show HN: i2forge – A Platform for Verified Reasoning
i2forge.com

Re: Show HN: i2forge – A Platform for Verified Reasoning

#2

Post by tromp »

> It occupies the place of Peano's * first axiom that 1 ∈ N. */

Natural numbers should start with 0 [0].

Suspiciously, the following lines in the proof can be entirely removed while still verifying:

    @func nat(x any) bool;
    term 1 nat;
[0] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...

Re: Show HN: i2forge – A Platform for Verified Reasoning

#3

Post by akiarie »

tromp wrote: post #2

> It occupies the place of Peano's * first axiom that 1 ∈ N. */ Natural numbers should start with 0 [0]. Suspiciously, the following lines in the proof can be entirely removed while still verifying: @func nat(x any) bool; term 1 nat; [0] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...

You raise two fine points.

> Natural numbers should start with 0 [0].

I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an early draft in which we were using 0 instead of 1: [0]. The reason we ended up going with 1 is we were imitating the structure of the proofs in Landau's "Foundations", and he uses 1 as his first number.

An interesting takeaway was the following. The way he structures his theorems and proofs, he makes use of his assumption that 0 is not a natural number. For example, Theorem 7 in the book is "y != x + y (for all natural numbers x, y)". So I found that sticking to my roots as a programmer (and admirer of Dijkstra) and insisting on zero-indexing led to more complicated theorem statements (e.g. "y != x + y for all natural numbers x, y > 0"). I'm not sure whether this is something structural about how the properties of natural numbers, integers, etc. relate; or whether it's an artefact of Landau's approach.

> Suspiciously, the following lines in the proof can be entirely removed while still verifying:

Suspicion warranted! The first (or zeroth) of these is a bug we hadn't fixed yet (see [1]). Our implementation is rather rough around the edges, but I've put a small fix for this—try again and tell me what you think.

The line "term 1 nat" interestingly isn't used in the theorem we've written, so it's more a mistake on our part for including it in the sample code. Good spot! See the language page [2] for an example where it is used.

As an aside, have you noticed that our proof style is based on what we call "Dijkstra-chaining"? Any thoughts on this? [3]

[0] https://paste.sr.ht/~akiarie/d7a2ae368faae4ba9a8bc13eeefcf18....

[1] https://todo.sr.ht/~lbnz/i2/1

[2] https://i2lang.org/#uses1

[3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/E...

Re: Show HN: i2forge – A Platform for Verified Reasoning

#4

Post by IshKebab »

akiarie wrote: post #3
tromp wrote: post #2

> It occupies the place of Peano's * first axiom that 1 ∈ N. */ Natural numbers should start with 0 [0]. Suspiciously, the following lines in the proof can be entirely removed while still verifying: @func nat(x any) bool; term 1 nat; [0] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...

You raise two fine points. > Natural numbers should start with 0 [0]. I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an early draft in which we were using 0 instead of 1: [0]. The reason we ended up going with 1 is we were imitating the structure of the proofs in Landau's "Foundations", and he uses 1 as his first number. An interesting takeaway was the following. The way he structure…

Presumably the theorem becomes `y >= x + y`?

Difficult to convince the entire field of mathematics that they are wrong though. It's hard enough to convince programmers - humans just have first=1 drummed into us so much it's like trying to convince a stone age man that the world is round.

I think mathematicians care even less because most of the problems with starting from 1 can be hand waved away when you're just writing non-executable formulas and can make up any syntax you want on the spot. If anything is really awkward with 1-based numbering, just change the notation so that it isn't! Programmers can't really do that so they feel the pain more.

Re: Show HN: i2forge – A Platform for Verified Reasoning

#5

Post by akiarie »

IshKebab wrote: post #4
akiarie wrote: post #3

Earlier quoted context omitted.

You raise two fine points. > Natural numbers should start with 0 [0]. I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an early draft in which we were using 0 instead of 1: [0]. The reason we ended up going with 1 is we were imitating the structure of the proofs in Landau's "Foundations", and he uses 1 as his first number. An interesting takeaway was the following. The way he structure…

Presumably the theorem becomes `y >= x + y`? Difficult to convince the entire field of mathematics that they are wrong though. It's hard enough to convince programmers - humans just have first=1 drummed into us so much it's like trying to convince a stone age man that the world is round. I think mathematicians care even less because most of the problems with starting from 1 can be hand waved away when you're just wri…

I think the challenge is it isn't completely obvious to me that starting with 0 is pedagogically correct, though it is so logically. `y >= x + y` is different from `y != x + y`; the former says that addition (of natural numbers) is monotonically increasing, the latter that there is no identity element. Is it possible that admitting an identity element is confusing for beginners? Or is this just a consequence of my own educational conditioning?

(For the record I think all the arguments Dijkstra gives for 0-indexing are correct. I just lack the mathematical intuition to see why the special case above appears to be one in which admission of 0 as complicates things.)

Re: Show HN: i2forge – A Platform for Verified Reasoning

#8

Post by akiarie »

__zack wrote: post #7

Interesting project. How does i2 compare with other languages used in verification / theorem proving, such as Agda, Lean, Isabelle, etc? From your site: > i2forge is a commercial venture, unlike i2 How are you planning to monetize i2forge?

> How does i2 compare with other languages used in verification?

I have to plead a measure of ignorance here as the context for my response, though we are working to understand the existing languages.

Perhaps what distinguishes i2 from the existing languages is we're treating this as an engineering rather than a science problem. We aren't trying to build up from the ideal logical system (which is maybe what Coq, Agda, Lean etc. do) but rather, viewing things pragmatically, trying to build a language that requires the least amount of investment for the average practicing mathematician to learn and begin using.

The sense I get (again appealing to ignorance) when I look at most of Coq-style options is that one has to learn type theory and/or constructivism before starting. In this way maybe we're closer to HOL and Isabelle.

Another angle is we're coming from a programming background, and view C as the model for what we're trying to achieve. C somehow captured all the essential capabilities of a Von Neumann machine at the right level of abstraction, and with a very "orthonormal" feature set, such that nearly every major system in the world is written in it or in a language based upon it. Our goal (which may greatly exceed our capacities) is to design something that does the same for maths.

> How are you planning to monetize i2forge?

We aren't sure about this at all. We're just convinced that we have unique insights into this problem and want to work on it full time, so we will be working towards monetising. One idea we've been playing around with is building tools for teachers, or for independent learners.

Re: Show HN: i2forge – A Platform for Verified Reasoning

#9

Post by akiarie »

practal wrote: post #6

I like the way you are thinking about this. And yes, formal math is the future! If you want to check out how to deal with quantification properly, or more generally with operators, without a need to explicitly introduce types, check out https://practal.com .

We're looking at this. Some very fascinating stuff. Somewhere at the beginning of "The Calculi of Lambda Conversion" Church talks about the fact that quantification can be reduced to lambdas. I have not read to the end of the paper (still learning these things step by step) and as we have struggled to understand how we should represent quantification, one of the things that became clear is the analogy between functions and quantifiers on the ground that both bind variables, so on the surface what you're talking about has the ring of truth.

Re: Show HN: i2forge – A Platform for Verified Reasoning

#10

Post by practal »

akiarie wrote: post #9
practal wrote: post #6

I like the way you are thinking about this. And yes, formal math is the future! If you want to check out how to deal with quantification properly, or more generally with operators, without a need to explicitly introduce types, check out https://practal.com .

We're looking at this. Some very fascinating stuff. Somewhere at the beginning of "The Calculi of Lambda Conversion" Church talks about the fact that quantification can be reduced to lambdas. I have not read to the end of the paper (still learning these things step by step) and as we have struggled to understand how we should represent quantification, one of the things that became clear is the analogy between functio…

Church tried to reduce logic to his invention, the untyped lambda calculus, but failed in a first attempt [1]. He then proceeded later on to invent the simple theory of types, [2], and type theory is pretty much a descendant of that. My argument with abstraction logic is that trying to use lambda+types for logic is actually misguided and overly restrictive. Abstraction logic is simpler, and can nevertheless also express variable binding naturally.

You are kind of lucky that you are relatively fresh to all this, so you can approach both type theory and abstraction logic with an open mind, and see for yourself which you find more appealing.

[1] S. C. Kleene, J. B. Rosser. The Inconsistency of Certain Formal Logics. Annals of Mathematics, 1935.

[2] Alonzo Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 1940.

Post reply on HN