18 ms·

Ah, I see what you mean now -- yeah, if you simply don't work in the domain of dependent type theory but instead choose something more suitable, then it's not a

by aseipp 10y ago

Ah, I see what you mean now -- yeah, if you simply don't work in the domain of dependent type theory but instead choose something more suitable, then it's not a problem, c.f. why I mentioned DTs still suffer from problems like equality being hairy. Not every approach is so unlucky. :) I thought you meant more generally in "general mathematics" where it does seem in some cases equality is kind of hazy, so I sort of misinterpreted. > True, but the need for higher-order mathematics in the modeling of computation in the first place originates with the choice of functions as models of computation... But perhaps I'm being unfair. While functions are not a very good abstraction for reasoning about computation, they are a very useful programming abstraction, and for end-to-end verification you must reason at the programming language level (although there may be better ways of doing that, too). I kind of left "higher order mathematics" a bit vague... Personally in all the proofs, etc I've needed you don't need to go as far as talking about topological spaces or n-categories or whatever, which is what I'd consider "higher order", but this is the space where a lot of the focus on wrangling equality, etc seems to come from, which is what I was getting at. Then again, most people using Coq heavily are probably exactly the people who care about this. :) I'm not one of those people, I just like programming. And personally I find the choice of functions, etc as a notion of computation quite powerful, even if it gets hairy sometimes! I suppose you could call it pidgeon-holing or laziness, but I tend to get a lot of insight from viewing mathematics from a computational, constructive point of view like this. I more use it as a "bridge" to get places rather than an overarching view of mathematics, I suppose, and I think it's quite useful at that (e.g. recently I found that I like the view of quotients in the computational, type-theoretic view rather than the 'quotients' of non-type-theory where you're really talking about partitions and equivalence classes, etc)... This is also probably partially due to the fact I've spent the majority of my programming career with systems like Haskell. So I'm fairly comfortable with "computational mathematics" from this POV.

pron 10y ago
"Computational mathematics" is indeed very interesting (and lies at the very core of some type theories), but as a developer rather than a logician, I'm less concerned with the foundations of mathematics and more concerned with the opposite problem: mathematical computation, namely how computation is represented mathematically rather than how math is represented computationally. Functions are a fundamental mathematical abstraction, and requiring them to be computable is interesting, but functions are not a fundamental computational concept, and going the other way to represent computations as functions is what complicates matters when reasoning about many kinds of algorithms, especially those that are not mappings of inputs to outputs. In other words, I don't think that an interesting way to apply computational concepts (of typed lambda calculus) to the foundations of mathematics is necessarily the best way to apply mathematical thinking to computation. "Computational math" may not be the right math for "mathematical computation". There's an example of this unjustified (although possibly true -- we don't know) reasoning in the introduction to the Lean paper: > In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The problem is that the kinds of computations relevant in the first case and the kinds of computation in the second case can be wildly different. Computations used in proofs are very much "functional" (map input to output). Computations in real-world software systems that really need formal verification rarely are. The most common type of computation in either category is the least common in the other, so the assumption that the same mathematical foundation (and/or the same tool) should be used for both is unjustified. While the authors use the term "in practice" to preface their statement, judging by their publication history, I'm a bit skeptical of their experience in verifying real-world software. Nevertheless, Lean does seem like a great way to learn about dependent types, and as you pointed out, the work on dependent types and their possible application in software verification is far from done, so it's very hard to judge at this point whether or not the direction is the right one. In the end, regardless of formalism, the proofs and techniques of software verification turn out to be very similar in all formalisms.

by aseipp 10y ago

pron 10y ago

"Computational mathematics" is indeed very interesting (and lies at the very core of some type theories), but as a developer rather than a logician, I'm less concerned with the foundations of mathematics and more concerned with the opposite problem: mathematical computation, namely how computation is represented mathematically rather than how math is represented computationally. Functions are a fundamental mathematical abstraction, and requiring them to be computable is interesting, but functions are not a fundamental computational concept, and going the other way to represent computations as functions is what complicates matters when reasoning about many kinds of algorithms, especially those that are not mappings of inputs to outputs. In other words, I don't think that an interesting way to apply computational concepts (of typed lambda calculus) to the foundations of mathematics is necessarily the best way to apply mathematical thinking to computation. "Computational math" may not be the right math for "mathematical computation". There's an example of this unjustified (although possibly true -- we don't know) reasoning in the introduction to the Lean paper: > In practice, there is not a sharp distinction between verifying a piece of mathematics and verifying the correctness of a system: formal verification requires describing hardware and software systems in mathematical terms, at which point establishing claims as to their correctness becomes a form of theorem proving. Conversely, the proof of a mathematical theorem may require a lengthy computation, in which case verifying the truth of the theorem requires verifying that the computation does what it is supposed to do. The problem is that the kinds of computations relevant in the first case and the kinds of computation in the second case can be wildly different. Computations used in proofs are very much "functional" (map input to output). Computations in real-world software systems that really need formal verification rarely are. The most common type of computation in either category is the least common in the other, so the assumption that the same mathematical foundation (and/or the same tool) should be used for both is unjustified. While the authors use the term "in practice" to preface their statement, judging by their publication history, I'm a bit skeptical of their experience in verifying real-world software. Nevertheless, Lean does seem like a great way to learn about dependent types, and as you pointed out, the work on dependent types and their possible application in software verification is far from done, so it's very hard to judge at this point whether or not the direction is the right one. In the end, regardless of formalism, the proofs and techniques of software verification turn out to be very similar in all formalisms.