3 ms·

Interesting project. How does i2 compare with other languages used in verification / theorem proving, such as Agda, Lean, Isabelle, etc? From your site: > i2f

by __zack 4y ago

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?

akiarie 4y ago
> 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.

by __zack 4y ago

akiarie 4y ago

> 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.