9 ms·

> Am I wrong? Is this not possible? Yes, you're wrong. I mean, I agree with you. This is the route we should commit to. Building up mathematical theories in

> Am I wrong? Is this not possible? Yes, you're wrong. I mean, I agree with you. This is the route we should commit to. Building up mathematical theories in a programming language. But I think you've reached the right conclusion for horribly confused reasons, and that you severely over-estimate the state of the art in CS. This over-estimation results in you not realizing why something like this could be a valuable tool within the world you describe. Perhaps I'm wrong, but here's what gives me this impression: > Write human-provable "test-cases" Since the article is discussing mathematics, I suppose here by proof you actually really honestly mean proof. So proof by "I worked through 6 examples and they all turned out OK so far"? That's not typically what a mathematician means when they say they proved something. Proofs can get horribly complicated in ways that test cases generally don't. > Writing functions, "unit tests", building on abstractions, and creating "libraries" do help. We all know this because it works well in CS. Yes, all of these things would be great. But it's REALLY not that simple. Formal verification of software systems remains a mostly academic pursuit. There's some promising early work, but almost none of "us" formally verify our software. It does NOT work well in CS. Not at the moment. And most things we do in CS are conceptually simpler than a lot of mathematics. So exploring alternative interfaces makes a lot of sense. > Is this not possible? Is there a reason as to why math and logic can't be expressed as an abstract programing language? They can be. It's horrendously verbose, and it's difficult to do novel work in such a formal setting. It does not work well in the same sense that it does not work well in CS -- you can do it, if you're willing to spend 10x the time/money/effort for the "good enough" version (in math, paper proofs; in CS, shippable but unverified code).

gravypod 10y ago
> I think the problem is that you don't understand what a real result looks like in math Unfortunetly I've been plauged with the task of reading some math papers to understand some things in the past. I still wake up in a cold sweat some times. > So proof by "I worked through 6 examples and they all turned out OK so far"? > That's not typically what a mathematician means when they say they proved something... I'm well aware. That's why I included the quote marks. I mean a logical proof based on the relation of this "function's" suppositions in relation to the rest of the "functions" it is integrated with providing context and mathematical relations to the other parts of the conjecture you're working on. > Formal verification of software systems remains a mostly academic pursuit. There's some promising early work, but almost none of "us" formally verify our software. > So no, you're wrong. It does NOT work well in CS. Not at the moment. I mean this is just blatantly wrong and ignoring the face of what I'm saying. I'm implying that 1) if you have a pinical example of computer science you can take a freshman-level CS student, give them a tour of the language, and let them loose on a problem and they'll understand what's going on. Some of the worlds most complex simulation sytems have children in highschool writing games in them. Things like Unity and Unreal engine representing thousands and thousands of manhours to create along with entire libraries of research, industry-funded experiments, and years of expertise. I'm saying that the common practices of programming can yield systems that are simple for anyone to maintain and work on. I can't say the same for mathematics. While I understand the concepts of derivatives, integrals, and calculus if tasked I'd most likely not be able to provide a formula to define the area of a new shape despite understanding the core material far better then most programmers understand the new project they've been flung into. 2) the concepts from computer science and programming can be adapted to suit math's needs and these adaptations can be fluid where novel augmentations of the processes that yield positive results can be further integrated into mathematics. Programming and computer science are quickly evolving fields and have a unique possition in that many people engage in them without formal training from a university because in most cases it's simple unneeded. You can pick up one book and then rely on the common goal of every computer scientist and programmer that came before you: abstraction of the concepts to yield a simple solution to arbitrarily complex problems. Because of this you can jump anywhere and pick up and run with your work. I'm not saying these ideas are directly applicable with no modification. What I am saying is "these are the ideas that make my field possible" and suggesting that standardizing practices in the Math-heavy fields would not be a bad thing especially if these same standardized practices have been used to great lengths in our field to produce a set of very positive outcomes.
- throwaway729 10y ago
  TL;DR: The idea you express -- a programming-like approach to mathematics -- has been around since the dawn of Computer Science. I could even make the case that this idea pre-dates the computer by a couple hundred years. There are literally hundreds of researchers around the world working toward this vision. But this remains a niche approach, and there are some very real hurdles to wide-spread use. Therefore, exploring different approaches is certainly justifiable. -- > Unfortunetly I've been plauged with the task of reading some math papers to understand some things in the past. I still wake up in a cold sweat some times. I'm with you there :-) Although it's perhaps telling that many CS papers are just as bad, if not worse, even when they come with code! Executable ideas aren't necessarily easier to understand... >> formal verification is a mostly academic pursuit > I mean this is just blatantly wrong It's really not though! Things have really picked up over the past 10 years, but a vast majority of the software we use -- and a vast majority of the software being created -- does not make significant use of formal proof. And certainly not the sort of functional correctness verification efforts that would be analogous to formalized mathematics. > Some of the worlds most complex simulation sytems have children in highschool writing games in them This is like saying that multivariate calculus is child's play because children can manipulate things in R3. There's a kernel of truth, but it's mostly wildly incorrect. Most Mathematicians generate proofs, not pretty simulations. Besides, and more to the point, those kids can do that precisely because those engines/frameworks/languages abstract away a lot of very difficult mathematics that they couldn't hope to understand! Which is exactly what the work described in the article could achieve, in a different domain and for a user at a different level of maturity. >I'm saying that the common practices of programming can yield systems that are simple for anyone to maintain and work on. And I'm saying that the history of formal verification in CS and proof assistants in mathematics provide direct, empirical evidence that this just isn't true. Doing formal mathematics in a proof assistant (aka programming language) is hard and time-consuming. Maybe one day soon it will be practical for most mathematicians, but that day is not today. >I'm not saying these ideas are directly applicable with no modification People have been trying your idea since literally the dawn of Computer Science. Look up "proof assistant" in Wikipedia. "No modification" is the under-statement of the century. Figuring out those modifications is an entire not-so-cottage industry in CS research. There are entire families of conferences dedicated to the topic. So again, I agree with you! But you're vastly under-estimating the difficulty of what you suggest, and as a result, disregard interesting and possibly complementary approaches.

gravypod 10y ago

> I think the problem is that you don't understand what a real result looks like in math Unfortunetly I've been plauged with the task of reading some math papers to understand some things in the past. I still wake up in a cold sweat some times. > So proof by "I worked through 6 examples and they all turned out OK so far"? > That's not typically what a mathematician means when they say they proved something... I'm well aware. That's why I included the quote marks. I mean a logical proof based on the relation of this "function's" suppositions in relation to the rest of the "functions" it is integrated with providing context and mathematical relations to the other parts of the conjecture you're working on. > Formal verification of software systems remains a mostly academic pursuit. There's some promising early work, but almost none of "us" formally verify our software. > So no, you're wrong. It does NOT work well in CS. Not at the moment. I mean this is just blatantly wrong and ignoring the face of what I'm saying. I'm implying that 1) if you have a pinical example of computer science you can take a freshman-level CS student, give them a tour of the language, and let them loose on a problem and they'll understand what's going on. Some of the worlds most complex simulation sytems have children in highschool writing games in them. Things like Unity and Unreal engine representing thousands and thousands of manhours to create along with entire libraries of research, industry-funded experiments, and years of expertise. I'm saying that the common practices of programming can yield systems that are simple for anyone to maintain and work on. I can't say the same for mathematics. While I understand the concepts of derivatives, integrals, and calculus if tasked I'd most likely not be able to provide a formula to define the area of a new shape despite understanding the core material far better then most programmers understand the new project they've been flung into. 2) the concepts from computer science and programming can be adapted to suit math's needs and these adaptations can be fluid where novel augmentations of the processes that yield positive results can be further integrated into mathematics. Programming and computer science are quickly evolving fields and have a unique possition in that many people engage in them without formal training from a university because in most cases it's simple unneeded. You can pick up one book and then rely on the common goal of every computer scientist and programmer that came before you: abstraction of the concepts to yield a simple solution to arbitrarily complex problems. Because of this you can jump anywhere and pick up and run with your work. I'm not saying these ideas are directly applicable with no modification. What I am saying is "these are the ideas that make my field possible" and suggesting that standardizing practices in the Math-heavy fields would not be a bad thing especially if these same standardized practices have been used to great lengths in our field to produce a set of very positive outcomes.

throwaway729 10y ago
TL;DR: The idea you express -- a programming-like approach to mathematics -- has been around since the dawn of Computer Science. I could even make the case that this idea pre-dates the computer by a couple hundred years. There are literally hundreds of researchers around the world working toward this vision. But this remains a niche approach, and there are some very real hurdles to wide-spread use. Therefore, exploring different approaches is certainly justifiable. -- > Unfortunetly I've been plauged with the task of reading some math papers to understand some things in the past. I still wake up in a cold sweat some times. I'm with you there :-) Although it's perhaps telling that many CS papers are just as bad, if not worse, even when they come with code! Executable ideas aren't necessarily easier to understand... >> formal verification is a mostly academic pursuit > I mean this is just blatantly wrong It's really not though! Things have really picked up over the past 10 years, but a vast majority of the software we use -- and a vast majority of the software being created -- does not make significant use of formal proof. And certainly not the sort of functional correctness verification efforts that would be analogous to formalized mathematics. > Some of the worlds most complex simulation sytems have children in highschool writing games in them This is like saying that multivariate calculus is child's play because children can manipulate things in R3. There's a kernel of truth, but it's mostly wildly incorrect. Most Mathematicians generate proofs, not pretty simulations. Besides, and more to the point, those kids can do that precisely because those engines/frameworks/languages abstract away a lot of very difficult mathematics that they couldn't hope to understand! Which is exactly what the work described in the article could achieve, in a different domain and for a user at a different level of maturity. >I'm saying that the common practices of programming can yield systems that are simple for anyone to maintain and work on. And I'm saying that the history of formal verification in CS and proof assistants in mathematics provide direct, empirical evidence that this just isn't true. Doing formal mathematics in a proof assistant (aka programming language) is hard and time-consuming. Maybe one day soon it will be practical for most mathematicians, but that day is not today. >I'm not saying these ideas are directly applicable with no modification People have been trying your idea since literally the dawn of Computer Science. Look up "proof assistant" in Wikipedia. "No modification" is the under-statement of the century. Figuring out those modifications is an entire not-so-cottage industry in CS research. There are entire families of conferences dedicated to the topic. So again, I agree with you! But you're vastly under-estimating the difficulty of what you suggest, and as a result, disregard interesting and possibly complementary approaches.