14 ms·

Proofs are Programs – 19th Century Logic and 21st Century Computing (2000) [pdf]

27182818284 10y ago
I had math professors that would express this sentiment in undergrad. It is very true. However, problem sets generally aren't graded like they're programs, haha.
tpetricek 10y ago
People like to see logic and computing in this way and the author is a great storyteller. But it is a somewhat misleading perspective that is kind of similar to "Whig historiography" (https://en.wikipedia.org/wiki/Whig_history https://en.wikipedia.org/wiki/Whig_history): > Whig is an approach to historiography that presents the past as an inevitable progression towards ever greater liberty and enlightenment, culminating in modern forms of liberal democracy and constitutional monarchy. Just replace the "greater liberty" bit with what computer scientists (and the author) argue is the right way of doing computer science today. I'd love to read a historical treatment of the topic that is written by someone who is a historian rather than computer scientist twisting history to support their world view.
- pron 10y ago
  I would recommend Andrew Hodges. Read this to get a taste: Did Church and Turing Have a Thesis about Machines?[1] (spoiler alert: probably) For the history of logic, Jean van Heijenoort's[2] annotated anthology, From Frege to Gödel[3] is fascinating. And, BTW, I think your hunch (about Whig history) is correct. [1]: http://www.turing.org.uk/publications/ct70.pdf http://www.turing.org.uk/publications/ct70.pdf [2]: https://en.wikipedia.org/wiki/Jean_van_Heijenoort https://en.wikipedia.org/wiki/Jean_van_Heijenoort [3]: https://www.amazon.com/Frege-Godel-Mathematical-1879-1931-Sciences/dp/0674324498 https://www.amazon.com/Frege-Godel-Mathematical-1879-1931-Sc...
- tikhonj 10y ago
  That's not a charitable interpretation ("twisting history to support their world view"), and your comment seems to be conflating the language-logic view itself with the history presented here. The relationship between programs and logic is compelling for many reasons and can stand independent of how the two happened to be developed; my take is that the historical story here—which is definitely too pat—is presented more as an illustration of the idea than anything else. This is no different than how math textbooks present the history of any particular mathematical abstraction or theorem: they don't go in depth on all the false starts and dead ends people explored before making real progress. That's certainly something interesting but it has no place—and no room—in textbooks dedicated to explaining abstractions. The simplified story of how something could have been developed is, I believe, more relevant to understanding the importance of an idea than the way it was actually developed. The real history is full of noise, a function of the person who first happened upon the idea. It's not hard to image thousands of alternate worlds where the exact development of an idea was slightly different, but reflecting the same fundamentals—those differences end up as irrelevant details due to chance.
  - pron 10y ago
    > This is no different than how math textbooks present the history of any particular mathematical abstraction or theorem: they don't go in depth on all the false starts and dead ends people explored before making real progress. That's true, but it is important to point out when the story is told in a specific way to promote a certain ideology. I'm not saying it's wrong to promote an ideology (on the contrary; ideology is often very important) or that it's rare, but readers should be aware that a certain ideology is being promoted. Wadler is trying to promote functional programming by presenting it as a natural result of logic, and in many ways the essence of his story is correct (from other, more neutral accounts that I've read). But what readers may not know is that logic has not been the only motivating force in theoretical computer science (nor the most powerful), that there are other useful analogies between computation and other phenomena, and that what's presented here is just one perspective on computation. For example, Turing, the father of theoretical computer science which only gets a brief mention in this account[1], turned his attention to neural networks, biological computation and possibly even quantum computation (although he died while working on some physics results). Much of the main thrust of theoretical computer science was similarly influenced by information theory and the search for the "physical laws" of computation which led to complexity theory, something that is nearly entirely missing from the logical treatment. [1]: Both Wadler and Bob Harper often try to downplay Turing's role for ideological reasons (which, I think, is pretty funny considering the history of computer science), and neglect to mention that Church's relatively narrow perspective caused him to miss something very basic about computation, while Turing, who was opposed to logicism[2], i.e. reducing math to logic, was able to therefore grasp something much more fundamental about computation than Church. Interestingly, Brouwer, who is another figure that provides inspiration to proponents of FP, actually did not fall into this trap, and had the philosophical breadth that had led him to come closer to Turing's more general view of computation than Church, by trying, like Turing, to think -- philosophically rather than formally -- how the mind of a mathematician works regardless of a specific formalism. [2]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf Some interesting quotes: > On 1 December 1933, the minutes in the Moral Science Club records: “A.M. Turing read a paper on ‘Mathematics and Logic’. He suggested that a purely logistic view of mathematics was inadequate; and that mathematical propositions possessed a variety of interpretations, of which the logistic was merely one.” > He was engaged in a program of putting Russell’s new logic into place, critiquing, not only its position or office, but perspectives on mathematics being forwarded by the “purely logistic” views. Turing was insisting that mathematical discourse stand on its own autonomous feet. And he was rejecting the idea that Principia — or any other construal of mathematics as a whole in terms of symbolic logic — offers mathematics a “foundation” of any ultimate or privileged sort, or reduces it to logic. A “purely logistic view” is but one (philosophically tendentious) “interpretation” among others, and is therefore “inadequate”. This is thoroughly consonant with the opening of Wittgenstein’s 1932 Cambridge lectures “Philosophy for Mathematicians” we have quoted above: Principia is simply part of mathematics, and there is nothing wrong with mathematics before its foundations are laid. > Turing developed an “anthropological” approach to the foundations of logic, influenced by Wittgenstein, in which “common sense” plays a foundational role.
- kmicklas 10y ago
  Ooof, this is too true. As someone greatly interested in type theory and the advancement of programming, I think this is definitely an issue to watch out for. Side note: an even better example than Whig history might be Marx's historical materialism. (Also an analysis I am sympathetic to but equally fraught with this peril.)
pron 10y ago
That's certainly a very language-and-logic perspective on things. But one of the reasons Church missed the general concept of computation whereas Turing didn't was precisely because Church was stuck in the formalism of logic, and couldn't recognize that computation extends well beyond it. So proofs are programs, but so are, say, metabolic networks, neuron networks, and just about any discrete dynamical system. But are metabolic networks proofs? That's not so clear, and therefore it's not so clear that there is a universal equivalence here.
- marcosdumay 10y ago
  > But are metabolic networks proofs? Are they not equivalent to computers running some program? Equivalence is transitive. But I don't think you will be able to get any useful proof from one of them. That's because they are hard to program, they are still running some proof.
  - pron 10y ago
    But a "computer running a program" is not an interesting proof of anything. The proof depends on how the program is written. For example, a program written in an untyped language encodes only a very trivial proof by the C-H correspondence (of `tt ⇒ tt` or something like that) even though it performs the same computation of a program written in another formalism that expresses a much more interesting proof. In other words, the proof does not lie in the dynamical process of computation, but in properties of the language used to express the computation. This is a much less universal claim.
- hiker 10y ago
  What is commonly known as Curry-Howard correspondence (the duality between programs/proofs, computing/math) actually goes way deeper. The reason is that "computation" is very useful concept but it has taken us ages to define what it means precisely. But that didn't stop people of reinventing it in other areas. Curry-Howard is only one of many other isomorphism between programs and other areas. See "Physics, Topology, Logic and Computation: A Rosetta Stone"[1] and in particular Table 4 on pg. 66. Curry-Howard correspondence is the last two columns of the table; the other three columns are other "correspondences" in topology, physics and category theory. [1] http://math.ucr.edu/home/baez/rosetta.pdf http://math.ucr.edu/home/baez/rosetta.pdf
agentultra 10y ago
I love Wadler's papers. He did one on Monads that was approachable and revealing for me. I also love logic and the predicate calculus. Highly recommend reading this one. :)
- michaelsbradley 10y ago
  Which paper?
  - agentultra 10y ago
    http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba...
- dualogy 10y ago
  Some of his conference talks can be found on YT too, recommended
anentropic 10y ago
shame about the misplaced apostrophes
deleted 10y ago
[deleted]
cr0sh 10y ago
This may be slightly OT - but the one thing I have always wondered about the 19th century is why Babbage didn't go down the route of Boolean logic/math for computation? Furthermore, why he didn't incorporate and use relays (from telegraphy)? For that matter, why didn't Hollerith? Ultimately, to me it seems all connected to this "fixed" idea (that is, thinking "inside the box") that computation was about numbers - that there was only calculation and tabulation - counting, iow. While Boole came up with the math/logic - few pursued the idea of making machines to work with it (a few -did- exist, but were obscure, iirc); embodying logic using electrical circuits would have to wait. Then there was the "revelation" of computation being about symbols, not numbers - which opened everything up. I'm just kinda rambling here; my apologies. And, hindsight is always easier than foresight, of course. It just bugs me, and makes me wonder what "obvious" ideas we are missing today, that will change the world, that we won't know until we look back. I guess I wonder why many of the most world changing ideas (in the long run) are often very simple, and why did it take so long for humanity to see/discover them? I wonder if anyone has studied this - of if it is something that can be studied...?
- DougBTX 10y ago
  > a few -did- exist, but were obscure, iirc In a similar vein, the next big thing has probably been discovered, it just isn't big yet.
- jdmichal 10y ago
  I would think that computers were being made to be useful first and foremost. And binary computing was not really useful for logic and number crunching until a number of advancements. Babbage analytical engine - 1833 Boolean algebra - 1847 two's complement - 1945
  - ZenoArrow 10y ago
    Your list is missing a very important advancement from 1937: https://en.m.wikipedia.org/wiki/A_Symbolic_Analysis_of_Relay_and_Switching_Circuits https://en.m.wikipedia.org/wiki/A_Symbolic_Analysis_of_Relay...
- 10y ago
didibus 10y ago
Write a program to prove another one. It's pretty cool in concept, but is it useful in practice?
- xj9 10y ago
  TDD, formal verification i'd say yes
  - didibus 10y ago
    I know TDD has gotten out of fashion, where people seem to acknowledge today that the right balance of tests is better, more practical, then a test first and test everything approach. Formal verification hasn't really caught on yet. The extra effort needed to formally prove even a trivial program seems to be too high for the value it gives to most stakeholders. I'm really hopeful for simpler methods of formalized proofs, or even automated testing. I think today, the practical cost is maybe still too high for people to care.
    - jononor 10y ago
      Property-based testing can sometimes be a practical step inbetween unit-testing and formal proofs. Scala is where this is most common/well-supported, I think http://www.scalatest.org/user_guide/property_based_testing http://www.scalatest.org/user_guide/property_based_testing
    - User23 10y ago
      Formal verification will never catch on, because it's silly and prohibitively difficult for all but the simplest programs. On the other hand, formal construction is an idea whose time is long overdue. Rather than asking if program text T satisfies predicate P, instead start with P and then construct a T mechanically such that it must satisfy P. The latter is a much easier task than the former. Sort of like how it's easy to know N is the product of two large primes if you just multiplied two large primes together to get it.
      - 10y ago
imode 10y ago
curry-howard and Wadler's "Propositions as Types" talk at StrangeLoop* opened my eyes pretty early on to the sweet, sweet utility of logic in my every day programming. it sounds odd to start with but I never realized why these things mattered prior to viewing this talk. props to wadler. best ~40 minutes I've ever spent. *https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU
- protomikron 10y ago
  Thank you, that was a delightful talk, I did not know Wadler was so enthusiastic (but I have to say, most logicians and theoretical computer scientists are).
jwtadvice 10y ago
Anyone really familiar with this: are non-constructive proofs, things like Cantor Diagonalization or Erdos's Probabilistic Method, programs? Are they just non-terminating programs? I can see Cantor Diagonalization as a non-terminating program really easily, but I don't understand what the Probabilistic Method looks like as a program.
- LolWolf 10y ago
  Sure, you can add an oracle for axiom of choice and you're done (note that AoC -> Excluded Middle). A proof is then "constructive" in the same way (e.g. Can be also written as a program, there).
- openasocket 10y ago
  Nit: I'm not sure I would consider Cantor Diagonalization non-constructive. I wouldn't consider it constructive either, though. It's used to prove things like the uncountability of the reals: how do you constructively prove that no bijection exists between the naturals and the reals?
- black_knight 10y ago
  Cantor's diagonalisation is certainly constructive. Given a a sequence of sequences of binary digits, it gives a way of constructing a sequence not occurring in the sequence of sequences. The resulting sequence is as computable as the input. But to answer your question: Many mathematicians regard their (classical) proofs as algorithms. They just allow themselves to use an oracle call for any well-formed question: Say I want to prove B. Then, at some point in my proof, I formulate a sentence A, and make a call to the oracle. My proof/algorithm then branches: in one branch I assume A is true, in the other I assume A is false. If I can continue such each branch gives B true, then my proof works (classically). [0] The constructive critique is that such an algorithm cannot be executed my humans, or turing machines for that matter. Also there is a whole continuum of stronger and stronger oracles below this ultimate oracle allowed by classical logic — which is an interesting continuum to study. Often one can locate an exact class of oracles needed for a given classical proof to work out. [0]: This is the «church encoding» version of the law of excluded middle: For all B, we have (A → B) → (¬A → B) → B, which is equivalent to the usual formulation (A ∨ ¬A).
mrcactu5 10y ago
i am having my doubts these days. i would like to read my programs as proofs. then I ask myself what is the Amazon.com front page proving? we talk about proof writing in Haskell or Agda. What about Python? Can we prove things there? And finally I think about the statements I would actually like to prove? Much of mathematics requires second order logic or beyond, such as the Fundamental Theorem of Calculus. So for me the triad between Math and Logic and Computer Science is less than air-tight and will remain that way.
- User23 10y ago
  The Amazon.com front page generating code is a proof relating some properties of its output to its input and that it halts. However it's also basically incomprehensible, so I doubt anyone alive could actually tell you precisely what it's proving. Your ability to prove something in any language is dependent on having a formal semantic for that language, or at least for a cognitively manageable subset that you're willing to restrict yourself to. The language semantics and memory model serve as axioms. Given how American programmers are trained, it's not realistic to expect them to be able to think of programs in a logical semantic way. There is something of an art to it and it's hard to learn a new way of thinking when you're satisfied with a way you already have. I agree that you can have an enjoyable hobby or make a living programming without really understanding what you're doing beyond intuitively and that's totally fine. Computing time is cheap and most applications don't cause any great harm when they behave in unintended ways. However the isomorphism between predicate calculus and computer programming isn't subjective. Programs really are proofs, just some of them are very sloppy.
- tunesmith 10y ago
  Amazon's front page proves that by typing in the amazon.com url, you get a page of whatever content amazon generates. Which isn't a very useful proof. Python is dynamically typed, so it doesn't prove much either. But in a statically typed language, if you have a method that takes an integer and returns a string, then you have proven you can generate a string from an integer. If it runs, then you have proven it. Granted, that's also not particularly useful, but it's proven if it compiles/runs. To prove, you need types. Typeless proofs/programs are just really general, not-very-useful proofs, same with dynamic typing. That's why static typing gets you a little closer to the correspondence/isomorphism. Dependent types gets you closer still - like, if you have a method that will only compile if the method takes an array of numbers, and returns only the subset of those numbers that are even - then the correspondence is starting to get a bit useful. Then you know your output won't have numbers that weren't in the input. I don't have much experience with this so I'm probably explaining it badly.
protomikron 10y ago
Does there exists research that uses results from computation theory and applies them to physics? Admittedly I am not sure what exactly I mean by that or what I am searching for, but I believe there is some deep relationship between limits in computation and limits about what one can say about the physical universe (which could be the same).
- hiker 10y ago
  "Physics, Topology, Logic and Computation: A Rosetta Stone"[1] might be a starting point. [1] http://math.ucr.edu/home/baez/rosetta.pdf http://math.ucr.edu/home/baez/rosetta.pdf

I had math professors that would express this sentiment in undergrad. It is very true. However, problem sets generally aren't graded like they're programs, haha.

tpetricek 10y ago

People like to see logic and computing in this way and the author is a great storyteller. But it is a somewhat misleading perspective that is kind of similar to "Whig historiography" (https://en.wikipedia.org/wiki/Whig_history https://en.wikipedia.org/wiki/Whig_history): > Whig is an approach to historiography that presents the past as an inevitable progression towards ever greater liberty and enlightenment, culminating in modern forms of liberal democracy and constitutional monarchy. Just replace the "greater liberty" bit with what computer scientists (and the author) argue is the right way of doing computer science today. I'd love to read a historical treatment of the topic that is written by someone who is a historian rather than computer scientist twisting history to support their world view.

pron 10y ago
I would recommend Andrew Hodges. Read this to get a taste: Did Church and Turing Have a Thesis about Machines?[1] (spoiler alert: probably) For the history of logic, Jean van Heijenoort's[2] annotated anthology, From Frege to Gödel[3] is fascinating. And, BTW, I think your hunch (about Whig history) is correct. [1]: http://www.turing.org.uk/publications/ct70.pdf http://www.turing.org.uk/publications/ct70.pdf [2]: https://en.wikipedia.org/wiki/Jean_van_Heijenoort https://en.wikipedia.org/wiki/Jean_van_Heijenoort [3]: https://www.amazon.com/Frege-Godel-Mathematical-1879-1931-Sciences/dp/0674324498 https://www.amazon.com/Frege-Godel-Mathematical-1879-1931-Sc...
tikhonj 10y ago
That's not a charitable interpretation ("twisting history to support their world view"), and your comment seems to be conflating the language-logic view itself with the history presented here. The relationship between programs and logic is compelling for many reasons and can stand independent of how the two happened to be developed; my take is that the historical story here—which is definitely too pat—is presented more as an illustration of the idea than anything else. This is no different than how math textbooks present the history of any particular mathematical abstraction or theorem: they don't go in depth on all the false starts and dead ends people explored before making real progress. That's certainly something interesting but it has no place—and no room—in textbooks dedicated to explaining abstractions. The simplified story of how something could have been developed is, I believe, more relevant to understanding the importance of an idea than the way it was actually developed. The real history is full of noise, a function of the person who first happened upon the idea. It's not hard to image thousands of alternate worlds where the exact development of an idea was slightly different, but reflecting the same fundamentals—those differences end up as irrelevant details due to chance.
- pron 10y ago
  > This is no different than how math textbooks present the history of any particular mathematical abstraction or theorem: they don't go in depth on all the false starts and dead ends people explored before making real progress. That's true, but it is important to point out when the story is told in a specific way to promote a certain ideology. I'm not saying it's wrong to promote an ideology (on the contrary; ideology is often very important) or that it's rare, but readers should be aware that a certain ideology is being promoted. Wadler is trying to promote functional programming by presenting it as a natural result of logic, and in many ways the essence of his story is correct (from other, more neutral accounts that I've read). But what readers may not know is that logic has not been the only motivating force in theoretical computer science (nor the most powerful), that there are other useful analogies between computation and other phenomena, and that what's presented here is just one perspective on computation. For example, Turing, the father of theoretical computer science which only gets a brief mention in this account[1], turned his attention to neural networks, biological computation and possibly even quantum computation (although he died while working on some physics results). Much of the main thrust of theoretical computer science was similarly influenced by information theory and the search for the "physical laws" of computation which led to complexity theory, something that is nearly entirely missing from the logical treatment. [1]: Both Wadler and Bob Harper often try to downplay Turing's role for ideological reasons (which, I think, is pretty funny considering the history of computer science), and neglect to mention that Church's relatively narrow perspective caused him to miss something very basic about computation, while Turing, who was opposed to logicism[2], i.e. reducing math to logic, was able to therefore grasp something much more fundamental about computation than Church. Interestingly, Brouwer, who is another figure that provides inspiration to proponents of FP, actually did not fall into this trap, and had the philosophical breadth that had led him to come closer to Turing's more general view of computation than Church, by trying, like Turing, to think -- philosophically rather than formally -- how the mind of a mathematician works regardless of a specific formalism. [2]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf Some interesting quotes: > On 1 December 1933, the minutes in the Moral Science Club records: “A.M. Turing read a paper on ‘Mathematics and Logic’. He suggested that a purely logistic view of mathematics was inadequate; and that mathematical propositions possessed a variety of interpretations, of which the logistic was merely one.” > He was engaged in a program of putting Russell’s new logic into place, critiquing, not only its position or office, but perspectives on mathematics being forwarded by the “purely logistic” views. Turing was insisting that mathematical discourse stand on its own autonomous feet. And he was rejecting the idea that Principia — or any other construal of mathematics as a whole in terms of symbolic logic — offers mathematics a “foundation” of any ultimate or privileged sort, or reduces it to logic. A “purely logistic view” is but one (philosophically tendentious) “interpretation” among others, and is therefore “inadequate”. This is thoroughly consonant with the opening of Wittgenstein’s 1932 Cambridge lectures “Philosophy for Mathematicians” we have quoted above: Principia is simply part of mathematics, and there is nothing wrong with mathematics before its foundations are laid. > Turing developed an “anthropological” approach to the foundations of logic, influenced by Wittgenstein, in which “common sense” plays a foundational role.
kmicklas 10y ago
Ooof, this is too true. As someone greatly interested in type theory and the advancement of programming, I think this is definitely an issue to watch out for. Side note: an even better example than Whig history might be Marx's historical materialism. (Also an analysis I am sympathetic to but equally fraught with this peril.)

pron 10y ago

That's certainly a very language-and-logic perspective on things. But one of the reasons Church missed the general concept of computation whereas Turing didn't was precisely because Church was stuck in the formalism of logic, and couldn't recognize that computation extends well beyond it. So proofs are programs, but so are, say, metabolic networks, neuron networks, and just about any discrete dynamical system. But are metabolic networks proofs? That's not so clear, and therefore it's not so clear that there is a universal equivalence here.

marcosdumay 10y ago
> But are metabolic networks proofs? Are they not equivalent to computers running some program? Equivalence is transitive. But I don't think you will be able to get any useful proof from one of them. That's because they are hard to program, they are still running some proof.
- pron 10y ago
  But a "computer running a program" is not an interesting proof of anything. The proof depends on how the program is written. For example, a program written in an untyped language encodes only a very trivial proof by the C-H correspondence (of `tt ⇒ tt` or something like that) even though it performs the same computation of a program written in another formalism that expresses a much more interesting proof. In other words, the proof does not lie in the dynamical process of computation, but in properties of the language used to express the computation. This is a much less universal claim.
hiker 10y ago
What is commonly known as Curry-Howard correspondence (the duality between programs/proofs, computing/math) actually goes way deeper. The reason is that "computation" is very useful concept but it has taken us ages to define what it means precisely. But that didn't stop people of reinventing it in other areas. Curry-Howard is only one of many other isomorphism between programs and other areas. See "Physics, Topology, Logic and Computation: A Rosetta Stone"[1] and in particular Table 4 on pg. 66. Curry-Howard correspondence is the last two columns of the table; the other three columns are other "correspondences" in topology, physics and category theory. [1] http://math.ucr.edu/home/baez/rosetta.pdf http://math.ucr.edu/home/baez/rosetta.pdf

agentultra 10y ago

I love Wadler's papers. He did one on Monads that was approachable and revealing for me. I also love logic and the predicate calculus. Highly recommend reading this one. :)

michaelsbradley 10y ago
Which paper?
- agentultra 10y ago
  http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba...
dualogy 10y ago
Some of his conference talks can be found on YT too, recommended

anentropic 10y ago

shame about the misplaced apostrophes

deleted 10y ago

[deleted]

cr0sh 10y ago

This may be slightly OT - but the one thing I have always wondered about the 19th century is why Babbage didn't go down the route of Boolean logic/math for computation? Furthermore, why he didn't incorporate and use relays (from telegraphy)? For that matter, why didn't Hollerith? Ultimately, to me it seems all connected to this "fixed" idea (that is, thinking "inside the box") that computation was about numbers - that there was only calculation and tabulation - counting, iow. While Boole came up with the math/logic - few pursued the idea of making machines to work with it (a few -did- exist, but were obscure, iirc); embodying logic using electrical circuits would have to wait. Then there was the "revelation" of computation being about symbols, not numbers - which opened everything up. I'm just kinda rambling here; my apologies. And, hindsight is always easier than foresight, of course. It just bugs me, and makes me wonder what "obvious" ideas we are missing today, that will change the world, that we won't know until we look back. I guess I wonder why many of the most world changing ideas (in the long run) are often very simple, and why did it take so long for humanity to see/discover them? I wonder if anyone has studied this - of if it is something that can be studied...?

DougBTX 10y ago
> a few -did- exist, but were obscure, iirc In a similar vein, the next big thing has probably been discovered, it just isn't big yet.
jdmichal 10y ago
I would think that computers were being made to be useful first and foremost. And binary computing was not really useful for logic and number crunching until a number of advancements. Babbage analytical engine - 1833 Boolean algebra - 1847 two's complement - 1945
- ZenoArrow 10y ago
  Your list is missing a very important advancement from 1937: https://en.m.wikipedia.org/wiki/A_Symbolic_Analysis_of_Relay_and_Switching_Circuits https://en.m.wikipedia.org/wiki/A_Symbolic_Analysis_of_Relay...
10y ago

didibus 10y ago

Write a program to prove another one. It's pretty cool in concept, but is it useful in practice?

xj9 10y ago
TDD, formal verification i'd say yes
- didibus 10y ago
  I know TDD has gotten out of fashion, where people seem to acknowledge today that the right balance of tests is better, more practical, then a test first and test everything approach. Formal verification hasn't really caught on yet. The extra effort needed to formally prove even a trivial program seems to be too high for the value it gives to most stakeholders. I'm really hopeful for simpler methods of formalized proofs, or even automated testing. I think today, the practical cost is maybe still too high for people to care.
  - jononor 10y ago
    Property-based testing can sometimes be a practical step inbetween unit-testing and formal proofs. Scala is where this is most common/well-supported, I think http://www.scalatest.org/user_guide/property_based_testing http://www.scalatest.org/user_guide/property_based_testing
  - User23 10y ago
    Formal verification will never catch on, because it's silly and prohibitively difficult for all but the simplest programs. On the other hand, formal construction is an idea whose time is long overdue. Rather than asking if program text T satisfies predicate P, instead start with P and then construct a T mechanically such that it must satisfy P. The latter is a much easier task than the former. Sort of like how it's easy to know N is the product of two large primes if you just multiplied two large primes together to get it.
    - 10y ago

imode 10y ago

curry-howard and Wadler's "Propositions as Types" talk at StrangeLoop* opened my eyes pretty early on to the sweet, sweet utility of logic in my every day programming. it sounds odd to start with but I never realized why these things mattered prior to viewing this talk. props to wadler. best ~40 minutes I've ever spent. *https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU

protomikron 10y ago
Thank you, that was a delightful talk, I did not know Wadler was so enthusiastic (but I have to say, most logicians and theoretical computer scientists are).

jwtadvice 10y ago

Anyone really familiar with this: are non-constructive proofs, things like Cantor Diagonalization or Erdos's Probabilistic Method, programs? Are they just non-terminating programs? I can see Cantor Diagonalization as a non-terminating program really easily, but I don't understand what the Probabilistic Method looks like as a program.

LolWolf 10y ago
Sure, you can add an oracle for axiom of choice and you're done (note that AoC -> Excluded Middle). A proof is then "constructive" in the same way (e.g. Can be also written as a program, there).
openasocket 10y ago
Nit: I'm not sure I would consider Cantor Diagonalization non-constructive. I wouldn't consider it constructive either, though. It's used to prove things like the uncountability of the reals: how do you constructively prove that no bijection exists between the naturals and the reals?
black_knight 10y ago
Cantor's diagonalisation is certainly constructive. Given a a sequence of sequences of binary digits, it gives a way of constructing a sequence not occurring in the sequence of sequences. The resulting sequence is as computable as the input. But to answer your question: Many mathematicians regard their (classical) proofs as algorithms. They just allow themselves to use an oracle call for any well-formed question: Say I want to prove B. Then, at some point in my proof, I formulate a sentence A, and make a call to the oracle. My proof/algorithm then branches: in one branch I assume A is true, in the other I assume A is false. If I can continue such each branch gives B true, then my proof works (classically). [0] The constructive critique is that such an algorithm cannot be executed my humans, or turing machines for that matter. Also there is a whole continuum of stronger and stronger oracles below this ultimate oracle allowed by classical logic — which is an interesting continuum to study. Often one can locate an exact class of oracles needed for a given classical proof to work out. [0]: This is the «church encoding» version of the law of excluded middle: For all B, we have (A → B) → (¬A → B) → B, which is equivalent to the usual formulation (A ∨ ¬A).

mrcactu5 10y ago

i am having my doubts these days. i would like to read my programs as proofs. then I ask myself what is the Amazon.com front page proving? we talk about proof writing in Haskell or Agda. What about Python? Can we prove things there? And finally I think about the statements I would actually like to prove? Much of mathematics requires second order logic or beyond, such as the Fundamental Theorem of Calculus. So for me the triad between Math and Logic and Computer Science is less than air-tight and will remain that way.

User23 10y ago
The Amazon.com front page generating code is a proof relating some properties of its output to its input and that it halts. However it's also basically incomprehensible, so I doubt anyone alive could actually tell you precisely what it's proving. Your ability to prove something in any language is dependent on having a formal semantic for that language, or at least for a cognitively manageable subset that you're willing to restrict yourself to. The language semantics and memory model serve as axioms. Given how American programmers are trained, it's not realistic to expect them to be able to think of programs in a logical semantic way. There is something of an art to it and it's hard to learn a new way of thinking when you're satisfied with a way you already have. I agree that you can have an enjoyable hobby or make a living programming without really understanding what you're doing beyond intuitively and that's totally fine. Computing time is cheap and most applications don't cause any great harm when they behave in unintended ways. However the isomorphism between predicate calculus and computer programming isn't subjective. Programs really are proofs, just some of them are very sloppy.
tunesmith 10y ago
Amazon's front page proves that by typing in the amazon.com url, you get a page of whatever content amazon generates. Which isn't a very useful proof. Python is dynamically typed, so it doesn't prove much either. But in a statically typed language, if you have a method that takes an integer and returns a string, then you have proven you can generate a string from an integer. If it runs, then you have proven it. Granted, that's also not particularly useful, but it's proven if it compiles/runs. To prove, you need types. Typeless proofs/programs are just really general, not-very-useful proofs, same with dynamic typing. That's why static typing gets you a little closer to the correspondence/isomorphism. Dependent types gets you closer still - like, if you have a method that will only compile if the method takes an array of numbers, and returns only the subset of those numbers that are even - then the correspondence is starting to get a bit useful. Then you know your output won't have numbers that weren't in the input. I don't have much experience with this so I'm probably explaining it badly.

protomikron 10y ago

Does there exists research that uses results from computation theory and applies them to physics? Admittedly I am not sure what exactly I mean by that or what I am searching for, but I believe there is some deep relationship between limits in computation and limits about what one can say about the physical universe (which could be the same).

hiker 10y ago
"Physics, Topology, Logic and Computation: A Rosetta Stone"[1] might be a starting point. [1] http://math.ucr.edu/home/baez/rosetta.pdf http://math.ucr.edu/home/baez/rosetta.pdf