3 ms·

From "Ask HN: Did studying proof based math topics make you a better programmer?" https://news.ycombinator.com/item?id=36463580 https://news.ycombinator.com/it

From "Ask HN: Did studying proof based math topics make you a better programmer?" https://news.ycombinator.com/item?id=36463580 https://news.ycombinator.com/item?id=36463580 : > Lean mathlib was originally a type checker proof assistant, but now leanprover-community is implementing like all math as proofs in Lean in the mathlib project Lean Mathlib is composed of executable proofs written in Lean: https://leanprover-community.github.io/mathlib-overview.html https://leanprover-community.github.io/mathlib-overview.html

eduhetxub 3y ago
Be careful. While a proof in Lean is executable (it is a script, so to speak) it is conceptually a sequence of references to tactics. Writing a Lean proof does involve a highly specialised form of functional programming, but I wouldn't be at all sure that becoming an expert in Lean would improve your programming skills across the board. Your comment also reminds me of the people who claim that the Curry-Howard isomorphism means "programming is math". It's not a claim that anyone should really be making in good faith. There's a lot more to programming than the lambda calculus.
- westurner 3y ago
  Verbal skills are apparently more predictive of programming career success than math scores. Is Quantum Logic the correct propositional logic? Is Quantum Logic a sufficient logic for all things? I'd much rather work with machine-checkable proofs; though Lean is not what I've been taught math in either. Coq-HoTT is written in Coq, not Lean. A tool that finds the correspondence between proofs as presented and checkable proofs in a reasonable syntax would be helpful, I think. If I start with "Why is 2+2=4?" [in this finite ring], I'm not sure how to find the relevant Lean code in Mathlib to prove my bias inductively, deductively, or abductively
  - 3abiton 3y ago
    > Verbal skills are apparently more predictive of programming career success than math scores. Curious about the references!
    - photonthug 3y ago
      I've heard this and always thought it was probably true even setting aside the soft skills part of the job, but that was before data engineering and data scientists were common titles. If it ever was true, the situation is probably more nuanced now than it used to be
      - westurner 3y ago
        I guess it means they're not testing on logic in the math exam, or are verbal scores predictive of coding but not logic scores; maybe it's more of a G factor.
  - isaacfrond 3y ago
    > Verbal skills are apparently more predictive of programming career success than math scores. This is an urban legend inspired by this article [1]. One problem with this research though is that it studies language learning. Not how good a programmer one becomes, and certainly not career success. [1]: Relating Natural Language Aptitude to Individual Differences in Learning Programming Languages. https://www.nature.com/articles/s41598-020-60661-8 https://www.nature.com/articles/s41598-020-60661-8
ratmice 3y ago
Not all lean proofs are actually computable, see the computable function link in the url you gave.
- westurner 3y ago
  Not all code functions are mathematical functions. An expression can describe a relation that is not a function per the definition like "a function always returns one output for one input". Function (mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) The Navier-Stokes equations are PDEs, not functions; but are they computable in Lean, or can algorithms for finding solutions be expressed in Lean? Lean docs > Missing undergraduate mathematics in mathlib: https://leanprover-community.github.io/undergrad_todo.html#:~:text=Multivariable%20calculus https://leanprover-community.github.io/undergrad_todo.html#:... Is ℯ^(2ί π x) a function? It's a complex function, but Geogebra draws it as a ~ (unit circle) + (y=0 if x > 0).
  - ratmice 3y ago
    What I mean is lean can prove things like one of cantors theorems, the proof of which requires you to derive from properties on a function f showing that there exists a function g inverse to f, and show something about the results of calling g. such a function in lean is considered non-computable by lean because it cannot be evaluated by lean since g has merely been shown to exist. Many proofs in lean however are computable, just not all.
    - westurner 3y ago
      I don't think SymPy has abstract Function attributes to reason about, but it does have limited reasoning about number classes given e.g. `x = Symbol('x', real=True)` SymPy docs > Writing Custom Functions > Easy Cases: Fully Symbolic or Fully Evaluated: https://docs.sympy.org/latest/guides/custom-functions.html#writing-custom-functions https://docs.sympy.org/latest/guides/custom-functions.html#w... If there is some sort of e.g. geometric correspondence, it could be possible for a Church-Turing classical computer to compute quantum functions (that return wave functions) that a Church-Turing-Deutsch quantum computer can compute; but otherwise Lean can't compute most quantum circuits either.

eduhetxub 3y ago

Be careful. While a proof in Lean is executable (it is a script, so to speak) it is conceptually a sequence of references to tactics. Writing a Lean proof does involve a highly specialised form of functional programming, but I wouldn't be at all sure that becoming an expert in Lean would improve your programming skills across the board. Your comment also reminds me of the people who claim that the Curry-Howard isomorphism means "programming is math". It's not a claim that anyone should really be making in good faith. There's a lot more to programming than the lambda calculus.

westurner 3y ago
Verbal skills are apparently more predictive of programming career success than math scores. Is Quantum Logic the correct propositional logic? Is Quantum Logic a sufficient logic for all things? I'd much rather work with machine-checkable proofs; though Lean is not what I've been taught math in either. Coq-HoTT is written in Coq, not Lean. A tool that finds the correspondence between proofs as presented and checkable proofs in a reasonable syntax would be helpful, I think. If I start with "Why is 2+2=4?" [in this finite ring], I'm not sure how to find the relevant Lean code in Mathlib to prove my bias inductively, deductively, or abductively
- 3abiton 3y ago
  > Verbal skills are apparently more predictive of programming career success than math scores. Curious about the references!
  - photonthug 3y ago
    I've heard this and always thought it was probably true even setting aside the soft skills part of the job, but that was before data engineering and data scientists were common titles. If it ever was true, the situation is probably more nuanced now than it used to be
    - westurner 3y ago
      I guess it means they're not testing on logic in the math exam, or are verbal scores predictive of coding but not logic scores; maybe it's more of a G factor.
- isaacfrond 3y ago
  > Verbal skills are apparently more predictive of programming career success than math scores. This is an urban legend inspired by this article [1]. One problem with this research though is that it studies language learning. Not how good a programmer one becomes, and certainly not career success. [1]: Relating Natural Language Aptitude to Individual Differences in Learning Programming Languages. https://www.nature.com/articles/s41598-020-60661-8 https://www.nature.com/articles/s41598-020-60661-8

ratmice 3y ago

Not all lean proofs are actually computable, see the computable function link in the url you gave.

westurner 3y ago
Not all code functions are mathematical functions. An expression can describe a relation that is not a function per the definition like "a function always returns one output for one input". Function (mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) https://en.wikipedia.org/wiki/Function_(mathematics) The Navier-Stokes equations are PDEs, not functions; but are they computable in Lean, or can algorithms for finding solutions be expressed in Lean? Lean docs > Missing undergraduate mathematics in mathlib: https://leanprover-community.github.io/undergrad_todo.html#:~:text=Multivariable%20calculus https://leanprover-community.github.io/undergrad_todo.html#:... Is ℯ^(2ί π x) a function? It's a complex function, but Geogebra draws it as a ~ (unit circle) + (y=0 if x > 0).
- ratmice 3y ago
  What I mean is lean can prove things like one of cantors theorems, the proof of which requires you to derive from properties on a function f showing that there exists a function g inverse to f, and show something about the results of calling g. such a function in lean is considered non-computable by lean because it cannot be evaluated by lean since g has merely been shown to exist. Many proofs in lean however are computable, just not all.
  - westurner 3y ago
    I don't think SymPy has abstract Function attributes to reason about, but it does have limited reasoning about number classes given e.g. `x = Symbol('x', real=True)` SymPy docs > Writing Custom Functions > Easy Cases: Fully Symbolic or Fully Evaluated: https://docs.sympy.org/latest/guides/custom-functions.html#writing-custom-functions https://docs.sympy.org/latest/guides/custom-functions.html#w... If there is some sort of e.g. geometric correspondence, it could be possible for a Church-Turing classical computer to compute quantum functions (that return wave functions) that a Church-Turing-Deutsch quantum computer can compute; but otherwise Lean can't compute most quantum circuits either.