My unusual hobby • Hacker News Board

Re: My unusual hobby

#91

Post by jacobolus » Sat, Nov 25, 2017, 10:09 PM UTC

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…

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 everything must be done in a purely abstract and formal way. Without any examples to test, it’s hard to notice gaps in logic.

According to Wikipedia this particular theorem was proved almost immediately (but not published) by Dedekind, and then 10 years later proved by a 19 year old student in Cantor’s seminar. It’s not clear whether more than a handful of people cared or worked on it in between.

As for Cantor being a leading mathematician of the day: most of the other mathematicians of his time regarded this whole mess to not be mathematics at all. Poincaré called Cantor’s set theory a “disease”. It wasn’t until several decades later that a broader group of mathematicians decided that roping in set theory allowed them to conveniently hand-wave away (“oh, the set theorists will take care of that part”) a lot of thorny questions, letting them get on with their work as they had before, but now with an deflective answer whenever anyone asked such questions. ;-)

Re: My unusual hobby

#92

Post by pbhjpbhj » Sat, Nov 25, 2017, 10:09 PM UTC

sls wrote: post #74

jloughry wrote: post #64

Earlier quoted context omitted.

It's pronounced like "cock". It's named after the animal, and that's how you say it in French. It's how people who use the tool say it.

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…

Quick look on YouTube, this guy says "cock" [short staccato 'k' at the end] https://www.youtube.com/watch?v=WFen8x66ETY and this guy https://www.youtube.com/watch?v=sW4uki0Fr8I - both apparently French (though the guy on the second one really sounds like he's faking it!).

In your example the 'o' is more precise and the 'k' is swallowed a little.

I'd expect they're different accents, perhaps your example is more Northern French (I really don't know).

Re: My unusual hobby

#93

Post by inopinatus » Sat, Nov 25, 2017, 10:14 PM UTC

jacquesm wrote: post #75

eqmvii wrote: post #56

Earlier quoted context omitted.

> Mathematicians don't just write down a proof and cross their fingers. On the flip side, this is exactly what a lot of lawyers do when writing contracts. Not necessarily maliciously or negligently, but it can still make for fun questions of interpretation when things don't go as expected.

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.

Re: My unusual hobby

#94

Post by pbhjpbhj » Sat, Nov 25, 2017, 10:18 PM UTC

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.

>"Are there mathematical proofs that are incapable of being expressed in Coq?" //

Like the proof that there are proofs incapable of being expressed in Coq?!

Re: My unusual hobby

#95

Post by rocqua » Sat, Nov 25, 2017, 10:21 PM UTC

fizixer wrote: post #63

amelius wrote: post #61

Reminds me of Principia Mathematica, where the author (Bertrand Russell) needs 379 pages to prove that 1+1=2. [1] > "From this proposition it will follow, when arithmetical addition has been defined, that 1 + 1 = 2." —Volume I, 1st edition, page 379. [1] https://en.wikipedia.org/wiki/Principia_Mathematica

Fun aside: I'd love to see the reaction of an applied-math class, like an engineering class, in which the instructor after having introduced the course, says, "let's go through some math prequisites for this class" and essentially starts reciting something equivalent to Principia Mathematica (without mentioning what he's trying to prove, meaning in a bottom-up fashion), - "If A is true, and B is true, then C is true"…

Do that to any pure math class and they will similarly walk out. You need to know where something abstract like this is going to follow at all.

Re: My unusual hobby

#96

Post by Wizek » Sat, Nov 25, 2017, 10:23 PM UTC

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…

Couldn't it be possible to unfold a proof by printing all the subsequent proof states one after the other? Wouldn't that be easier to follow?

Re: My unusual hobby

#97

Post by rocqua » Sat, Nov 25, 2017, 10:33 PM UTC

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…

The basic issue lies with `decidability'. Generally we want type systems to tell us whether our program is well typed. However as your type-system becomes `too expressive' it starts to become much harder to determine if a program is well typed.

When finally a type system becomes so expressive as to be Turing complete, you get 'undecidable types'. Those are the types that correspond to undecidable programs for Turing machines.

A consequence is that any `sound' typing system will have to reject some programs that actually are `well typed'. This is why many type systems have a "Just trust me, this is fine" option. Like casting in C/C++ and unsafe in rust.

To fully eliminate those "Just trust me" and still accept all well typed programs you'd need to accept potentially never ending type-checking (or else you'd have solved the halting problem).

Re: My unusual hobby

#98

Post by [deleted] » Sat, Nov 25, 2017, 10:38 PM UTC

rocqua wrote: post #95

fizixer wrote: post #63

Earlier quoted context omitted.

Fun aside: I'd love to see the reaction of an applied-math class, like an engineering class, in which the instructor after having introduced the course, says, "let's go through some math prequisites for this class" and essentially starts reciting something equivalent to Principia Mathematica (without mentioning what he's trying to prove, meaning in a bottom-up fashion), - "If A is true, and B is true, then C is true"…

Do that to any pure math class and they will similarly walk out. You need to know where something abstract like this is going to follow at all.

[deleted]

Re: My unusual hobby

#99

Post by seanwilson » Sat, Nov 25, 2017, 10:40 PM UTC

wolfgke wrote: post #59

seanwilson wrote: post #30

Earlier quoted context omitted.

> Putting aside their steep learning curve, formal proof methods do not guarantee that the code you've written is bug free. People seem to always bring this up but what's better? Verified code is about as close as you're ever going to get to bug free. If you're doing a large proof, getting the specification wrong and not eventually noticing while working on the proof isn't common. You'll likely have something that is…

> I haven't heard of any examples of complex verified programs where later someone found a huge flaw in the specification. Look at > https://www.krackattacks.com/ "The 4-way handshake was mathematically proven as secure. How is your attack possible? The brief answer is that the formal proof does not assure a key is installed only once. Instead, it merely assures the negotiated key remains secret, and that handshake m…

> I personally would consider this as a clear example of a huge flaw in a specification where a correctness proof was done on.

Awesome, thanks for the recent example. My point is people seem to always bring up that specifications may have flaws as if this makes verifying code pointless. The guarantee of correctness is still an order of magnitude better than e.g. using unit tests and I'd wager it isn't common that specifications are wrong in a critical way. It's difficult to make a mistake specifying that a program should not have buffer overflows and out of range errors for instance.

The WPA2 flaw is an example of a specification missing an important property as opposed to a property being described incorrectly. People seem to jump on the latter the most I find as if it's common.

Re: My unusual hobby

#100

Post by fizixer » Sat, Nov 25, 2017, 10:43 PM UTC

auggierose wrote: post #88

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…

These notions are actually becoming more and more intermixed. You could say today that interactive theorem proving (what is done in a proof assistant) is an extension of automated theorem proving, as for example the Isabelle proof assistant has very strong support for proving intermediate theorems automatically.

Thanks, I think this is a good example of what I'm looking for.

One key ingredient is the presence of a logic inference engine (and not for type inference only, as in Coq, Haskell).

- If your system doesn't have a logic inference engine, it's a vanilla proof-assistant (Coq).

- If it has one, it's one of two:

  - a partially-automated theorem prover, (Isabelle)

  - a fully-automated theorem prover

P.S.: Wait a minute. It just occurred to me, is Coq using its Hindley-Milner Type Inference engine as a Logic Inference engine for verifying constructed proofs of theorems and propositions? (is that the killer idea?)