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

My unusual hobby

stephanboyer.com

Post reply on HN
Print view View original

41–50 of 157 posts

Re: My unusual hobby

#41

Post by fizixer »

So I'm wondering what is the bridge between "proof-assistant" and "automated (or partially automated) theorem prover".

As someone with "journalistic" (but fairly in-depth) knowledge about these topics, my guess is that something like a proof-assistant will have to be paired up with some kind of logic programming system (like Prolog, or a kanren-derived system or something).

I guess then the problem of combinatorial explosion in logic search translates directly to the combinatorial explosion of proof-steps in a proof assistant. Hence my mention of partially-automated (more doable than fully-automated).

Probably some kind of a "database of facts" would also be involved, making it an expert system (reminds me of metamath [1]).

Is it fair to say, partially-automated theorem proving is a fairly advanced version (and not without added complexity) of a proof-assistant, and will help ease some of the grunt work involved in using a proof-assistant by hand?

[1] http://us.metamath.org/

Re: My unusual hobby

#42

Post by yaseer »

lordleft wrote: post #27

Are there mathematical proofs that are incapable of being expressed in Coq? Isn't there a limit to kind of ideas a computer could verify? Curious about the boundaries of this language.

This question gets at the heart of computation, logic and provability.

Coq is based on a logic system called the "Calculus of constructions" https://en.wikipedia.org/wiki/Calculus_of_constructions. As such it has the same limitations as that logical system.

Most notably, Gödel's incompleteness theorems place a limit on what's provable in Coq, or indeed many other systems.

There are various kinds of logic systems, each with different kinds of 'power'. Power is a double-edge sword in logic systems, as with power comes the capacity to introduce paradoxes and inconsistencies.

As with programming languages, certain logic systems and automated logics are suited for particular cases. For example, there is a system 'MetiTarski' like a Domain Specific Language, designed to prove theorems about real-valued special functions.(https://www.cl.cam.ac.uk/~lp15/papers/Arith/).

Re: My unusual hobby

#43

Post by curryhoward »

yaseer wrote: post #35

If you're a programmer that's not tried theorem proving before, I highly recommend giving it a go. It gave me the same 'thrill' I got when I first started programming as a 14-year old and realised a new way of thinking. I find it sharpens your mind in a new, and different way - that's really an exciting feeling. I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Coq howe…

> I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense.

Just curious, what makes Isabelle easier to read? I haven't tried it.

Re: My unusual hobby

#44

Post by yaseer »

curryhoward wrote: post #43
yaseer wrote: post #35

If you're a programmer that's not tried theorem proving before, I highly recommend giving it a go. It gave me the same 'thrill' I got when I first started programming as a 14-year old and realised a new way of thinking. I find it sharpens your mind in a new, and different way - that's really an exciting feeling. I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Coq howe…

> I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Just curious, what makes Isabelle easier to read? I haven't tried it.

Isabelle comes with a proof language layer Isar, designed specifically for readability: https://isabelle.in.tum.de/Isar/

The structure of Isar proofs then more closely resemble a traditional mathematical proof, with a formalisation close to natural language. You can see the example from Wikipedia:

https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)

As you can see, the overall structure of the proof is clearer, and you have less dependency of seeing the proof state to understand the proof.

The downside to Isabelle is that it introduces a dual syntax, with certain sections written in quotes. There's more to learn syntax and concept wise, but I think it's worth the extra effort for a clearer proof.

EDIT: Linked to Wikipedia page for formatting.

Re: My unusual hobby

#45

Post by dllthomas »

seanc wrote: post #31
voxl wrote: post #15

Earlier quoted context omitted.

Nothing guarantees that code is bug free. We will always have to interact with hardware, and although we can have high confidence in the hardware the physical world has a habit of changing out from under us. Your argument is very strange. We use type systems not because we think we'll write perfect code, but because we know it will reduce the likelihood of making mistakes in our code (at least, when that type system…

"Beware of bugs in the above code; I have only proved it correct, not tried it. " - Don Knuth

Of course, Knuth's proof was not mechanically checked...

Re: My unusual hobby

#46

Post by raphlinus »

fizixer wrote: post #41

So I'm wondering what is the bridge between "proof-assistant" and "automated (or partially automated) theorem prover". As someone with "journalistic" (but fairly in-depth) knowledge about these topics, my guess is that something like a proof-assistant will have to be paired up with some kind of logic programming system (like Prolog, or a kanren-derived system or something). I guess then the problem of combinatorial e…

I've done a bit of work on a "next generation" Metamath, Ghilbert[1], but have come to the conclusion that it's too ambitious to do as a part-time project. People might find it interesting, though, because it attempts to take interactivity to a higher level than Metamath, and is (imho) a cleaner language.

[1] http://ghilbert.org/

Re: My unusual hobby

#48

Post by yodsanklai »

I've never managed to have fun with Coq even though I really tried. I did tons of exercises and labs. On the other hand, I do love (functional) programming, logic and maths in general.

It's almost like you get the bad side of programming (time-consuming, tedious) without the reward (seeing your program doing cool things). And you don't get the satisfaction of doing maths either. At least I don't. Maybe I didn't try hard enough.

What is very interesting though is to learn about type theory and the Curry Howard isomorphism.

Re: My unusual hobby

#50

Post by Someone »

david-gpu wrote: post #2

I had to take a semester on formal proofs using Coq, the same tool the article talks about. Putting aside their steep learning curve, formal proof methods do not guarantee that the code you've written is bug free. They only guarantee that the code follows the requirements you defined given the conditions you also set on your inputs. You can think of it as a mathematical proof of your postconditions will hold given th…

”formal proof methods do not guarantee that the code you've written is bug free. They only guarantee that the code follows the requirements you defined given the conditions you also set on your inputs.”

I think you are mixing “bug” with “out of spec”. If you ask me to write a perfect chess program, you can’t say it’s a bug if it can’t play go.

Bad or incomplete requirements are a problem, but that’s a different problem from “bugs”.

Post reply on HN