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

151–157 of 157 posts

Re: My unusual hobby

#151

Post by jmite »

mcguire wrote: post #10

And this... " To give you an idea of what an actual proof looks like in Coq, below is a proof of one of the easier lemmas above. The proof is virtually impossible to read without stepping through it interactively, so don’t worry if it doesn’t make any sense to you here. " is why Coq is not one of my favorite tools. A proof consists of two things: the "proof state"---a statement of what you know at a given point--and…

What is your favorite tool? Agda? I've been finding it much nicer to work with, but the ecosystem is just not there yet.

Re: My unusual hobby

#152

Post by Zimm_i48 »

qznc wrote: post #20
mcguire wrote: post #10

And this... " To give you an idea of what an actual proof looks like in Coq, below is a proof of one of the easier lemmas above. The proof is virtually impossible to read without stepping through it interactively, so don’t worry if it doesn’t make any sense to you here. " is why Coq is not one of my favorite tools. A proof consists of two things: the "proof state"---a statement of what you know at a given point--and…

I you prefer readable proofs, try Isabelle or Lean.

You can certainly do readable proofs in Coq the way you would do them in Isabelle, but this requires stating intermediate states explicitly (with assert e.g.) and Coq users rarely do that (mainly because readability is not their goal, I guess).

Re: My unusual hobby

#153

Post by maxhallinan »

A lot of these comments are focused on the merits of Coq and some of the mathematical details of your post. As someone who has no experience with Coq and little experience with mathematical proofs, I want to add an additional perspective. This is a pretty cool hobby. It's really nice to hear about hobbies that aren't motivated by ambitions of profit or fame. Thanks for sharing!

Re: My unusual hobby

#154

Post by runeks »

edanm wrote: post #84
j2kun wrote: post #5

> What's really amazing to me is that Stephen Kleene probably proved this without the help of a computer, but I was able to verify it with the highest possible scrutiny. It's as if he wrote an impressive program without ever having run it, and it turned out not to have any bugs! This offhand comment (which we can all forgive) makes it seem like mathematics happens in a vacuum. I can understand the temptation to think…

One very interesting experience for me was recently relearning set theory from a textbook. It talked a bit about the history of the Schröder–Bernstein theorem, a fundamental (and relatively "simple" sounding) result in Set theory. What I found interesting was that this originally stated, but not proved, by Cantor. Then a few semi-flawed attempts at proofs were made (flawed in the sense that they relied on other axiom…

If something that looks obviously true is hard to prove using some given language, couldn’t that be a sign that we’re using the wrong language to construct the proof?

Could there exist a language where these sorts of proofs become easier to write, because that language captures the problem in a better way?

Re: My unusual hobby

#155

Post by runeks »

mcguire wrote: post #10

And this... " To give you an idea of what an actual proof looks like in Coq, below is a proof of one of the easier lemmas above. The proof is virtually impossible to read without stepping through it interactively, so don’t worry if it doesn’t make any sense to you here. " is why Coq is not one of my favorite tools. A proof consists of two things: the "proof state"---a statement of what you know at a given point--and…

Are there languages that model proofs as pure functions? I.e. instead of modifying some implicit state, you pass existing proofs as arguments to other proofs that define these existing proofs as assumptions to itself.

So, a proof would be a pure function, taking a number of assumptions as arguments, and in order to write this proof you must first pass proofs of the assumptions to it as arguments (and then you can reference these proven assumptions in the body of the proof when needed).

Re: My unusual hobby

#156

Post by bordercases »

sundarurfriend wrote: post #148
bordercases wrote: post #146

Earlier quoted context omitted.

> My experience is: formally proving something in Coq is not a prerequisite for understanding it, but understanding it is a prerequisite for formally proving it in Coq. So if you get Coq to accept your proof, it's a good sign that you understand every detail. Such tasks are called "orienting tasks" in the cognitive science/human learning literature, and are useful because what it means to "understand" something is qu…

Thanks for the link, that was quite interesting. I love the format that the article takes, as well. I liked the superscript note numbers that xkcd's whatif blog uses, this is another implementation of that, executed very well.

It makes printing a bitch but overall I wouldn't mind if more articles were formatted like that, yeah.

Re: My unusual hobby

#157

Post by amazingman »

inopinatus wrote: post #93
jacquesm wrote: post #75

Earlier quoted context omitted.

There is a nice parallel between the legal profession and programming. Programmers write software in such a way that they try (if they're any good) to reduce the number of assumptions made and the number of bugs and the ambiguities in their code. Failure to do so results in undefined behavior, crashing code and in internet facing code in possibly being hacked. Lawyers write code into contracts. Good lawyers try to do…

The law is not a programming language. Believing so is a common misconception amongst engineers, but representing it as such is likely (as I have said in this forum before) to lead to disappointment, frustration, anger, needless bickering, extended conflict, and vexatiously long, hard to read, and mostly unenforceable contracts.

It’s a useful metaphor, if used judiciously. The law may not be programming, but it could be argued that it is engineering.
Post reply on HN