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

141–150 of 157 posts

Re: My unusual hobby

#141

Post by mietek »

curryhoward wrote: post #32
zaptheimpaler wrote: post #22

Cool post! The stuff about Curry-Howard was really interesting and relates to a question i have been thinking about. But I'm a novice when it comes to the theory of type systems or theorem provers. Maybe someone here can enlighten me? As type systems become more complex (like say in Scala or Haskell), they move towards having specialized syntax and weird hacks to express what are arguably simpler logical theorems/inv…

> so why can't we have a programming language that gives you a full blown logic system Most dependently typed programming languages, including Coq, give you the ability to basically "do logic" in a mostly unrestricted way. There are a few challenges that come to mind with making a practical programming language that can also do arbitrary math: a) For the language to be useful for proving things, it needs to be strong…

> For the language to be useful for proving things, it needs to be strongly normalizing. That means all programs halt—otherwise, you could trivially prove any proposition. Unfortunately that limits its utility as a general purpose programming language.

It’s not true that a strongly normalising language must be limited in utility. See section 4 on codata of Turner’s 2004 “Total functional programmming” for more information.

https://github.com/mietek/total-functional-programming/blob/...

Re: My unusual hobby

#142

Post by daxfohl »

jacobolus wrote: post #91
edanm wrote: post #84

Earlier quoted context omitted.

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…

The reasons such proofs are non-obvious is because they are proofs about the relative “size” of hypothetical infinite objects of a type we can never actually grapple with in any physical way even in principle, but only posit as a thought experiment, based on invented axioms in an invented logical system. There’s no concrete computation involved (or even possible) in this kind of context, and no practical examples. So…

Which even amplifies the observation. Not only is the process of proving a theorem more complex than it looks in retrospect, but the whole process of deciding whether a theorem or even a whole field of math is even useful or not can be driven by chance over a time span of decades. What is now "topology" was kicked around for many years with many approaches before a general agreement that open sets formed the most useful basis (heh). Advanced textbook authors regularly have to cut topics from subsequent editions of the book, because what seemed promising 30 years ago turned into a dead end. So math is far from the discrete list of topics and answers that it seems to be when you're picking out classes in your syllabus.

Re: My unusual hobby

#143

Post by aswanson »

curryhoward wrote: post #8
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…

(OP here.) Fair enough—thanks for the thoughtful clarification. By the way, I'm a big fan of your "Math ∩ Programming" articles. People who found my blog interesting will certainly think the same of yours: https://jeremykun.com/

Big fan of his, and your work as well.

Re: My unusual hobby

#144

Post by auggierose »

somenewacc wrote: post #138
auggierose wrote: post #18

Earlier quoted context omitted.

Formally proving something is just very expensive. The difference between the cost of an informal understanding of the correctness of your code, and the cost of formally proving it in a theorem prover is usually at least one order of magnitude (if you are lucky). A compiler though with a type system actually REDUCES your cost. So these are very different beasts.

Type checking your code is, in a sense, a formal proof. That is, your types encode theorems, and the compiler check them. The article actually alludes to this, linking to this: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Yeah, I should have been more specific in my comment: I don't mean type systems like in Agda or Idris or Coq ..., but where writing down the types is not a big deal, because otherwise you are doing theorem proving with all the associated costs.

In short: I like both my type systems and my theorem proving without any involvement of Curry-Howard :D

Re: My unusual hobby

#145

Post by [deleted] »

daxfohl wrote: post #142
jacobolus wrote: post #91

Earlier quoted context omitted.

The reasons such proofs are non-obvious is because they are proofs about the relative “size” of hypothetical infinite objects of a type we can never actually grapple with in any physical way even in principle, but only posit as a thought experiment, based on invented axioms in an invented logical system. There’s no concrete computation involved (or even possible) in this kind of context, and no practical examples. So…

Which even amplifies the observation. Not only is the process of proving a theorem more complex than it looks in retrospect, but the whole process of deciding whether a theorem or even a whole field of math is even useful or not can be driven by chance over a time span of decades. What is now "topology" was kicked around for many years with many approaches before a general agreement that open sets formed the most use…

[deleted]

Re: My unusual hobby

#146

Post by bordercases »

curryhoward wrote: post #12
j2kun wrote: post #7

My question for the author: does implementing a proof formally in Coq honestly give you a better understanding of the theorem/proof? It would seem to me that, if you're filling in details from an existing proof or making some existing formal (in the math sense) intuition more formal (in the Coq sense), there's not much deep insight to gain from implementing a proof in Coq.

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. For the domain theory proof I discussed in the article, formalizing it in Coq absolutely helped me understand it because: a) Merely formalizing the definitions wa…

> 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 quite nebulous and we often fool ourselves when we actually think we understand something. They also allow us to test understanding outside of the domain it's supposed to be applied in, which is useful if the real situation is noisy, messy or costly.

Scott H Young explains the psychology of the problem well: https://www.scotthyoung.com/blog/2017/06/13/how-much-do-you-...

Re: My unusual hobby

#147

Post by carapace »

I've been working in a CPS Joy variant, deriving recursive functions on trees and such. I've noticed that the code always works the first time. So far my "data" on this phenomenon is still too anecdotal to get excited, but I wanted to mention it (here where people might be interested.) It surprised me at first, but then I realized that this is part of the promise of Backus' Functional Programming: being able to do algebra to derive programs gives you error-free code that doesn't require tests.

It leads me to speculate... what if I don't need types to write correct software? I assumed I would implement typing and type inference (like Factor language already has) at some point. But if the code has no bugs without it... YAGNI?

My reasoning goes like this: Let's postulate that we have a library of functions, each of which has the quality Q of being error-free. If we derive new functions from the existing ones by a process that preserves Q, so that new functions are all also error-free, then we cannot have errors in our code, just user error. I.e. the user can present bad inputs, but no other source of error exists (other than mechanical faults.) This would be a desirable state of affairs. Now if the Q-preserving new-function-deriving process doesn't require types to work, then we don't need them. Whether or not typing helps prevent user error is another question. Personally, I lean toward defining user error as UI error, but I am ranging far from my original point now.

(If you're interested: https://github.com/calroc/joypy/tree/master/docs Still very DRAFT versions. https://github.com/calroc/joypy/blob/master/docs/3.%20Develo... )

Re: My unusual hobby

#148

Post by sundarurfriend »

bordercases wrote: post #146
curryhoward wrote: post #12

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. For the domain theory proof I discussed in the article, formalizing it in Coq absolutely helped me understand it because: a) Merely formalizing the definitions wa…

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

Re: My unusual hobby

#149

Post by dwheeler »

mcguire wrote: post #127
sls wrote: post #74

Earlier quoted context omitted.

Not really, the English word "cock" has a very different vowel than the French "coq" - https://youtu.be/bIraCzL3dtI?t=4s is a pretty fair exemplar. It's a lot more like the "o" in "joke". (edit: maybe you're English? Some English accents of England would articulate "cock" very close to French "coq" and "joke" would be far away. Apologies, one really does need to specify which "English" is meant, and I should have see…

Perhaps more like "Coke"?

I pronounce it as "coke", for fairly obvious reasons :-).

Re: My unusual hobby

#150

Post by wolfgke »

seanwilson wrote: post #101
marcosdumay wrote: post #60

Earlier quoted context omitted.

> Verified code is about as close as you're ever going to get to bug free. Code verified by legible proofs is safer than merely verified. The quality of the verification language matters, it's not only the programming language.

> Code verified by legible proofs is safer than merely verified. The quality of the verification language matters, it's not only the programming language. If the specifications are human legible though, why do you care if the proof (which is checked for you by the machine) is legible? The main point of formal methods is to remove any doubt there are errors in the proof so it's an order of magnitude safer than relying…

> If the specifications are human legible though, why do you care if the proof (which is checked for you by the machine) is legible?

Because it is a goal of any science not to make a correct model, but also to get a high-level understanding what this model is about. Feel free to call this high-level understanding "what it is really about a "meta-property" of the model, which we also would like to have.

Post reply on HN