3 ms·

> 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

> 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.

klodolph 10y ago
I'm not sure what to make of these comments here. What Linus does is a mix of software engineering, project management, people management, and product management. Computer science might be a distant fifth, as is the case with most people in the industry. There's no sense in poking fun at homomorphic encryption for being "hip". It's hip because it's a result that computer scientists have been trying to discover for many years, one with tons of potential applications. I also have to agree that formal verification is largely an academic endeavor. Static analysis is taking off these days but that's not formal verification in any sense. There are a few projects here and there that are formally verified, and certainly there are tools for formal verification, but I've met precious few people in industry who even know how to use proof assistants. This includes my experience working with aerospace clients. Formally verified components, either hardware or software, tend to be small. The first formally verified kernel, for example, is the seL4 microkernel and verification took from 2006 to 2009. Suffice it to say there are few formally verified kernels floating around.
throwaway729 10y ago
TL;DR: If you want to do mathematics in a programming language as you suggest, then you need programming language that can express proof. Mathematics without proofs isn't mathematics. The ergonomics issues present in all of the existing languages for describing mathematical proofs are one way to motivate the work described in the article. > I'm not too fond of academic-anything. There's a difference between recognizing your personal tastes and being dismissive of entirely reasonable enterprises. > Most papers are bad, period. Most jounals are bad, period. Most software is bad, period. Most documentation of software is bad, period. Especially when written by 20-somethings straight out of university, which describes the vast majority of paper writers in academia. ...what's your point? > I think Linus is more of a computer science then someone who comes up with a new cryptography algorithm What benefit is there in re-defining extremely well-established terms? It doesn't actually serve to convince anyone of anything, and confuses conversations. > I'm not talking about formal verification when I talk about computer science/programming methods for representing ideas. So then you dismiss mathematics as a discipline? Because writing some code and some test cases is not mathematics. Modern Mathematics means proofs. Period. Proof assistants are languages we've invented for describing proofs. They are literally exactly what you've asked for in your original post. And they're pretty difficult to use. So exploring different approaches for describing mathematical structures and proofs makes a lot of sense. > 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. Yes, I acknowledged that we've made tremendous progress! But formal verification is still extremely resource intensive and extremely rare in software. > You've got planes flying in the air by Boeing that are almost verified completely. Where did you even get this idea? It isn't true. Every line of code might've been run through Coverity or whatever. Some static analysis is very different from verification of functional correctness properties. > Also, in math your proof is your program so this is an entierly different issue. Yes, this is exactly my point! To do math like programming, you need a language for describing proofs. All of the languages that exist for doing this are difficult to use. Maybe visual languages could help out here. > I'm saying they can benifit from the abstractions they stand on to create further experimentation for themselves. You're tying to argue that the success of modern programming practices indicates that we can do the same in math. But 40 years of proof assistants remaining niche demonstrate this simply isn't true. It's a good idea, but it's not easy to get right. > I'm not talking about formal verification. I'm taking about the ways we express our ideas. In mathematics, proofs are the critical piece of output. Expressing proofs is step zero toward "expressing our ideas" in mathematics. If you want to "do mathematics" in a language, as you suggest here, your language needs to be able to express proofs. > Computer Science != formal verification. And math != hacking out code. > I think your "formal verification is largely an academic endevour" takes the cake on that one. Okay. When was the last time you wrote production code that had a functional correctness proof? What percentage of software written yesterday would you guess or one day will have a functional correctness proof? Or, to borrow you point about children, when was the last time a high school student wrote a proof in a proof assistant (i.e. did math in a programming language)?

klodolph 10y ago

I'm not sure what to make of these comments here. What Linus does is a mix of software engineering, project management, people management, and product management. Computer science might be a distant fifth, as is the case with most people in the industry. There's no sense in poking fun at homomorphic encryption for being "hip". It's hip because it's a result that computer scientists have been trying to discover for many years, one with tons of potential applications. I also have to agree that formal verification is largely an academic endeavor. Static analysis is taking off these days but that's not formal verification in any sense. There are a few projects here and there that are formally verified, and certainly there are tools for formal verification, but I've met precious few people in industry who even know how to use proof assistants. This includes my experience working with aerospace clients. Formally verified components, either hardware or software, tend to be small. The first formally verified kernel, for example, is the seL4 microkernel and verification took from 2006 to 2009. Suffice it to say there are few formally verified kernels floating around.

throwaway729 10y ago

TL;DR: If you want to do mathematics in a programming language as you suggest, then you need programming language that can express proof. Mathematics without proofs isn't mathematics. The ergonomics issues present in all of the existing languages for describing mathematical proofs are one way to motivate the work described in the article. > I'm not too fond of academic-anything. There's a difference between recognizing your personal tastes and being dismissive of entirely reasonable enterprises. > Most papers are bad, period. Most jounals are bad, period. Most software is bad, period. Most documentation of software is bad, period. Especially when written by 20-somethings straight out of university, which describes the vast majority of paper writers in academia. ...what's your point? > I think Linus is more of a computer science then someone who comes up with a new cryptography algorithm What benefit is there in re-defining extremely well-established terms? It doesn't actually serve to convince anyone of anything, and confuses conversations. > I'm not talking about formal verification when I talk about computer science/programming methods for representing ideas. So then you dismiss mathematics as a discipline? Because writing some code and some test cases is not mathematics. Modern Mathematics means proofs. Period. Proof assistants are languages we've invented for describing proofs. They are literally exactly what you've asked for in your original post. And they're pretty difficult to use. So exploring different approaches for describing mathematical structures and proofs makes a lot of sense. > 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. Yes, I acknowledged that we've made tremendous progress! But formal verification is still extremely resource intensive and extremely rare in software. > You've got planes flying in the air by Boeing that are almost verified completely. Where did you even get this idea? It isn't true. Every line of code might've been run through Coverity or whatever. Some static analysis is very different from verification of functional correctness properties. > Also, in math your proof is your program so this is an entierly different issue. Yes, this is exactly my point! To do math like programming, you need a language for describing proofs. All of the languages that exist for doing this are difficult to use. Maybe visual languages could help out here. > I'm saying they can benifit from the abstractions they stand on to create further experimentation for themselves. You're tying to argue that the success of modern programming practices indicates that we can do the same in math. But 40 years of proof assistants remaining niche demonstrate this simply isn't true. It's a good idea, but it's not easy to get right. > I'm not talking about formal verification. I'm taking about the ways we express our ideas. In mathematics, proofs are the critical piece of output. Expressing proofs is step zero toward "expressing our ideas" in mathematics. If you want to "do mathematics" in a language, as you suggest here, your language needs to be able to express proofs. > Computer Science != formal verification. And math != hacking out code. > I think your "formal verification is largely an academic endevour" takes the cake on that one. Okay. When was the last time you wrote production code that had a functional correctness proof? What percentage of software written yesterday would you guess or one day will have a functional correctness proof? Or, to borrow you point about children, when was the last time a high school student wrote a proof in a proof assistant (i.e. did math in a programming language)?