3 ms·

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

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
> 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... I'm not too fond of academic-anything. Most papers are bad, period. Most jounals are bad, period. That's when taken in retrospect to this "good/bad" dichotomy. There are good and bad things in most of these things though that you and I can recognize. Sadly, Computer Science in adacemia is little math. In industry it means something completely different. I think Linus is more of a computer science then someone who comes up with a new cryptography algorithm, or homomorphic encryption method, or whatever is "hip" these days. > 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. I'm not talking about formal verification when I talk about computer science/programming methods for representing ideas. Also, formal-verification isn't an academic endevour. You've got a CPU in your system that is all formal verification of VHDL or Verilog. You've got planes flying in the air by Boeing that are almost verified completely. But I don't think formal verification is the most important! I think the way we represent out ideas in a clear and understandable fashon is important. My complaints are about language, not proof or semantics. Also, in math your proof is your program so this is an entierly different issue. > 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. I'm not saying a highschooler is Donald Knuth. I'm saying they can benifit from the abstractions they stand on to create further experimentation for themselves. One they, I do think, they will become Donald Knuths with better understandings of these building blocks they have access to. Do you think someone who has never touched a game engine will have an easier time understanding what a game engine does then someone who worked with them since they were in their early teens? I fully expect highschools who like math to be able to experiment with the implications of math just as currently a highschooler to likes computers can experiment easily with the implecation of computer programs. > 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. I'm not talking about formal verification. I'm taking about the ways we express our ideas. Computer Science != formal verification. I am talking about how programmers express their ideas and the steps of solving a problem. > "No modification" is the under-statement of the century. I think your "formal verification is largely an academic endevour" takes the cake on that one.

gravypod 10y ago

> 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... I'm not too fond of academic-anything. Most papers are bad, period. Most jounals are bad, period. That's when taken in retrospect to this "good/bad" dichotomy. There are good and bad things in most of these things though that you and I can recognize. Sadly, Computer Science in adacemia is little math. In industry it means something completely different. I think Linus is more of a computer science then someone who comes up with a new cryptography algorithm, or homomorphic encryption method, or whatever is "hip" these days. > 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. I'm not talking about formal verification when I talk about computer science/programming methods for representing ideas. Also, formal-verification isn't an academic endevour. You've got a CPU in your system that is all formal verification of VHDL or Verilog. You've got planes flying in the air by Boeing that are almost verified completely. But I don't think formal verification is the most important! I think the way we represent out ideas in a clear and understandable fashon is important. My complaints are about language, not proof or semantics. Also, in math your proof is your program so this is an entierly different issue. > 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. I'm not saying a highschooler is Donald Knuth. I'm saying they can benifit from the abstractions they stand on to create further experimentation for themselves. One they, I do think, they will become Donald Knuths with better understandings of these building blocks they have access to. Do you think someone who has never touched a game engine will have an easier time understanding what a game engine does then someone who worked with them since they were in their early teens? I fully expect highschools who like math to be able to experiment with the implications of math just as currently a highschooler to likes computers can experiment easily with the implecation of computer programs. > 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. I'm not talking about formal verification. I'm taking about the ways we express our ideas. Computer Science != formal verification. I am talking about how programmers express their ideas and the steps of solving a problem. > "No modification" is the under-statement of the century. I think your "formal verification is largely an academic endevour" takes the cake on that one.