The Evolution of Lisp (1993) [pdf] • Hacker News Board

Re: The Evolution of Lisp (1993) [pdf]

#11

Post by catnaroek » Sat, Aug 05, 2017, 10:39 PM UTC

reikonomusha wrote: post #9

fizixer wrote: post #6

Off-topic, just had this (micro)-epiphany that I wanted to share: It is well-known that a majority of programmers dread mathematics beyond something basic like high-school math, sometimes even less. What these programmers don't know is that a significant fraction of mathematicians (probably majority of them) who haven't been involved with programming, computers, computer algebra systems etc, have a similar dread abou…

I would certainly say programmers are not doing constructive math because most programmers' programs don't at all resemble any sort of rigorous proof. In fact, most professional, non-computer-scientist programmers write programs that are hacked up things that "work good enough".

Most programmers, whether professionals or not, and also whether computer scientists or not.

Re: The Evolution of Lisp (1993) [pdf]

#12

Post by catnaroek » Sat, Aug 05, 2017, 10:48 PM UTC

fizixer wrote: post #10

omaranto wrote: post #8

Earlier quoted context omitted.

I doubt any of the "many" people that say that programming is more mathematically rigorous than mathematics are mathematicians. For mathematicians rigor is about proof and they would never say that a discipline that usually does not involve writing proofs is more rigorous than mathematics. Maybe these people mean that formally verified programming is more rigorous than mathematics. That seems reasonable, but it is a…

What I said is along the lines of 'every program is a proof' and what people like Philip Wadler say that we should treat propositions (essentially theorems) as types and programs as proofs. Now, where the mathematicians disagree-with/dislike such an idea has something to do with the question "If a program is a proof, what is the theorem?". Since we can have buggy programs, the norm rather than the exception, in my op…

(0) To view programs as proofs, you need to first view programming languages as logics. Alas, when (or even if!) you view any general-purpose programming language as a logic, you'll find out that it contains lots of junk theorems that nobody actually wants to consider theorems.

(1) Don't conflate “rigorous” with “mechanized”. Rigor is a discipline that rules out invalid reasoning.

Re: The Evolution of Lisp (1993) [pdf]

#13

Post by omaranto » Sun, Aug 06, 2017, 3:03 AM UTC

fizixer wrote: post #10

omaranto wrote: post #8

Earlier quoted context omitted.

I doubt any of the "many" people that say that programming is more mathematically rigorous than mathematics are mathematicians. For mathematicians rigor is about proof and they would never say that a discipline that usually does not involve writing proofs is more rigorous than mathematics. Maybe these people mean that formally verified programming is more rigorous than mathematics. That seems reasonable, but it is a…

What I said is along the lines of 'every program is a proof' and what people like Philip Wadler say that we should treat propositions (essentially theorems) as types and programs as proofs. Now, where the mathematicians disagree-with/dislike such an idea has something to do with the question "If a program is a proof, what is the theorem?". Since we can have buggy programs, the norm rather than the exception, in my op…

So you weren't saying that programmers are being rigorous when they write programs, but just that computers are rigorous when they execute programs? I guess I wouldn't really argue with that.

Re: The Evolution of Lisp (1993) [pdf]

#14

Post by tunesmith » Sun, Aug 06, 2017, 5:50 AM UTC

fizixer wrote: post #10

omaranto wrote: post #8

Earlier quoted context omitted.

I doubt any of the "many" people that say that programming is more mathematically rigorous than mathematics are mathematicians. For mathematicians rigor is about proof and they would never say that a discipline that usually does not involve writing proofs is more rigorous than mathematics. Maybe these people mean that formally verified programming is more rigorous than mathematics. That seems reasonable, but it is a…

What I said is along the lines of 'every program is a proof' and what people like Philip Wadler say that we should treat propositions (essentially theorems) as types and programs as proofs. Now, where the mathematicians disagree-with/dislike such an idea has something to do with the question "If a program is a proof, what is the theorem?". Since we can have buggy programs, the norm rather than the exception, in my op…

It doesn't really mean much, though, if the working program (proof) corresponds to a theorem like "Given an Int, I can turn it into some other kind of Int", or "Given some sort of String, it's possible to turn it into a Boolean", or "Given an arbitrary input, I can yield some sort of arbitrary output". Those theorems are rather pointless. That's what most programs "as proofs" are like, where the value in them is in the side effects rather than their types. Now, when dependent types become more of a thing in the industry, maybe we can argue that our programs are getting more rigorous.

Re: The Evolution of Lisp (1993) [pdf]

#15

Post by agumonkey » Sun, Aug 06, 2017, 6:39 AM UTC

fizixer wrote: post #6

Off-topic, just had this (micro)-epiphany that I wanted to share: It is well-known that a majority of programmers dread mathematics beyond something basic like high-school math, sometimes even less. What these programmers don't know is that a significant fraction of mathematicians (probably majority of them) who haven't been involved with programming, computers, computer algebra systems etc, have a similar dread abou…

There's some truth to that. Math is paper computation. But it's also between the usual computation and the metalevel.

Look at how lambda calculus "functions" have been done in Java, who had OO and methods (~function) but had to reify lambdas in crude way. Proper math mindset allowed people to use these functions in a more abstract setting to do more with less.

Also after struggling with abstract algebra for long, I finally view these sorts of things as just another encoding of information as a dual of your problem. Modeling. It's a bit sacralized because either mathematicians are too much in love with their field or the rest of the world looks at it with ignorant eyes. It's beautiful, versatile and powerful, but approached the wrong way, it appears as more than it is.

In the end I believe that the two fields blend into one. I'm very curious to read HoTT for instance.

Re: The Evolution of Lisp (1993) [pdf]

#16

Post by googoo00 » Sun, Aug 06, 2017, 1:56 PM UTC

This appears to be an attack file.

Objects with Javascript code (34): [10, 16, 18, 22, 26, 30, 38, 44, 50, 56, 64, 70, 88, 94, 98, 120, 126, 132, 136, 138, 144, 161, 165, 167, 169, 174, 176, 180, 182, 184, 192, 214, 221, 225]

Recommend pdftops!

Re: The Evolution of Lisp (1993) [pdf]

#17

Post by jgalt212 » Sun, Aug 06, 2017, 2:17 PM UTC

googoo00 wrote: post #16

This appears to be an attack file. Objects with Javascript code (34): [10, 16, 18, 22, 26, 30, 38, 44, 50, 56, 64, 70, 88, 94, 98, 120, 126, 132, 136, 138, 144, 161, 165, 167, 169, 174, 176, 180, 182, 184, 192, 214, 221, 225] Recommend pdftops!

someone please elaborate on this.

Re: The Evolution of Lisp (1993) [pdf]

#18

Post by kazinator » Sun, Aug 06, 2017, 3:48 PM UTC

fizixer wrote: post #6

Off-topic, just had this (micro)-epiphany that I wanted to share: It is well-known that a majority of programmers dread mathematics beyond something basic like high-school math, sometimes even less. What these programmers don't know is that a significant fraction of mathematicians (probably majority of them) who haven't been involved with programming, computers, computer algebra systems etc, have a similar dread abou…

Programming is like mathematics and logic only when what you're programming is deterministic: repeatable results given repeated inputs, where run-time doesn't matter so much. There is other programming, like real-time shit. (There, other mathematics applies, not to mention statistics; but you're not programming directly in that mathematics.)

An operating scheduler can be regarded as a mathematical function, which chooses an element from a set. But then that choice has an impact on how the system performs under various conditions, which is pretty chaotic and doesn't follow in nice, obvious ways from that neat set-theoretic function.