Holbert: An Interactive Theorem Prover | Hacker News Reader

Holbert: An Interactive Theorem Prover

github.com

68 pointsfennecs9 comments

> Unlike conventional theorem provers, Holbert’s term language is just the untyped lambda calculus. While this technically makes the logic unsound, it is much simpler to use as a pedagogical tool.

I am not sure if it is very pedagogical to teach an unsound logic. How about you try a sound one? No types required: https://obua.com/publications/philosophy-of-abstraction-logi...

I've come to the conclusion that Abstraction Logic (AL) is actually the golden middle between FOL (first-order logic) and HOL (simply-typed higher-order logic with Henkin semantics): You can view it both as FOL plus operators/general variable binding, and as HOL minus static types!

Why would you even consider using an unsound logic?

I’m a 3rd year PhD student in formal verification and for the life of me I can’t imagine why anyone would choose to use an unsound logic. I must be missing something very obvious. Is it, IDK, “sound as long as you don’t reason about some very specific kind of formula which can be easily avoided”, or something like that?

When you create a new logic with certain applications in mind, it might be unsound at some intermediate steps, like you can have bugs in a program. But yeah, I don't think there is much use for an unsound logic per se.

The usual justification, within PL Design community is that, similar to Russell 's Paradox, it's said that the anomaly caused by the unsound logic does not come up in practical situations. For example, some (and definitely most if not all mainstream) languages admit `Type: Type` i.e. `Type` itself is a type within the formalism. Of course, this is unsound and one common work-around is to use universe polymorphism such as `Type n: Type (level-suc n)`. But this comes with its own design issues as now you may need to pass level to each type (depends on the language, situation etc). So, some decide, since (as per this reasoning) absurd situations implied by "Type: Type" don't come up in practical situations, it's better have a simpler and more understandable yet unsound Type Theory. (But of course, an inconsistent theory can prove any claim, which is a huge problem in and of itself)

I have to note that I personally do not agree with this reasoning, yet afaik this is one of the justifications used to introduce rules to TT of a PL that is known to be unsound.

Realistically, it all depends on what you want to do with the type system. If you want to have a general purpose programming language that is not restricted by logical technicalities not well-understood by programmers, maybe it's better to admit "Type: Type" or similar. If you want to have a dependently typed programming language where any runtime program can potentially be a compile-time program, you may need more guarantees (e.g. you may need to know certain functions will halt).

Because, as that quoted sentence points out, the logic itself is simpler and the creators think that makes it easier to use for teaching.

Taken to an extreme, if all you want to show off is how proofs are constructed, then whether or not your logic is actually sound doesn't matter. Since the goal of the tool isn't correct proofs, the proofs don't need to have any soundness properties.

This looks rather dense, and I wish I had the time and pre-requisite knowledge to parse it all. I feel like you might get more attention to this if you had some sort of benchmark, a metric or method of comparing your logic to FOL and HOL and highlighting the major impact. A way of formalizing this "golden middle" you mention in your comment. Similar to how machine learning papers include benchmarks, or how new frameworks / technologies often include a table of comparisons to other tech in the space.

Don't worry about it, I've showed it to the best people in the field (you would think), and haven't gotten much of a response out of most of them so far. It is a VERY conservative field. At least nobody so far said it's wrong. I am starting to submit now to conferences, let's see how long it takes until people realise what they've got here.

This is not a push-button technology like machine learning. You need to either experience using the logic, which is difficult right now, because there is no proof assistant yet implementing it (there will be something in a few months, I hope). Or you understand the arguments I make in the paper, which so far only two other people sort of have, both of which have a Ph.D. in the field.

But let me assure you, this is the simplest logic out there. If you have any questions, I'll be happy to answer them!

Much more documentation and tooling for this is necessary. It will take some time until it is accessible to most, but that time will come.

I wish you the best of luck, it looks like a ton of work, and while I won't pretend to be an expert, I thought it was quite impressive. Automated theorem proving is in its infancy so I'd imagine it's hard to find the right audience, but submitting it to conferences seems like a good bet!

Thanks! But it is actually an old field by now, and there are quite a few conferences for it. Although automated theorem proving and interactive theorem proving have developed on different tracks, they are slowly converging in the last 15 years or so.

Reply on news.ycombinator.com