3 ms·

I have contributed to proof assistants, and while programming is part of mathematics, it is not all of it. Obviously, a proof assistant is a program, but its co

• ndriscoll 2y ago
  I didn't say you always need to phrase things in those terms, merely that it can be useful to not try to avoid them (and I wish tutorials wouldn't obscure it). It's like how geometers use d/dx as an element of the tangent space, but they don't treat it as some quirk to ignore. They actually use the fact that it's an operator too. It makes things easier. Obviously you don't need to do that with every vector space you'll ever encounter. My original reply was to someone who thought proofs are all unit valued, which is the sort of confusion you get when these systems try to shy away from the programming part. The point was that proofs are things that a programmer ought to feel to be concrete, not just some trickery with type aliases of unit.
  • auggierose 2y ago
    > My original reply was to someone who thought proofs are all unit valued That is the danger if you get too married to the idea of proofs as programs, and think about it like a programmer, not a mathematician. Listen, if thinking about proofs as programs helps you, great! Personally, I never found it helpful, and it never helped me solve anything.