4 ms·

Are you familiar with homotopy type theory? One of its proponents, Fields medalist Vladimir Voevodsky, has stated that his contributions are part of a “personal

Are you familiar with homotopy type theory? One of its proponents, Fields medalist Vladimir Voevodsky, has stated that his contributions are part of a “personal mission” to bring mathematics into a new age of formal verification [1]. I’d be curious to know how this compares to LEAN. [1] https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins

deleted 5y ago
[deleted]
mhh__ 5y ago
I am kind of sceptical of these verified-mathematics projects in the sense that my litmus is whether I could easily verify my workings rather than the proofs I rely upon, but nonetheless I have enormous respect for those doing this work and really hope it comes to fruition. I really hope this work trickles down to our programming - state machine problems are basically "solved" (for my needs at least), but more complex programs are really hard to prove.
- pramodbiligiri 5y ago
  When you say that state machine problems are basically solved, are you referring to any tools that you're using to reason about them?
  - mhh__ 5y ago
    By solved I really mean "in commercial use", there's probably a lot of research let to be done, but people are already verifying TLA+ specs all day everyday.
- jkhdigital 5y ago
  I'm a PhD student in computer science, and after spending some time on this subject I'm pretty well convinced that parts of mathematics and CS are converging towards a more unified foundational framework that will benefit both fields tremendously. In a nutshell, the key challenge is taking the core of complexity theory (which is easy to formalize in terms of state machines) and migrating it into the language(s) of category/type theory (which is much more modular/compositional). A couple interesting recent works in this area: Categorical Complexity: https://www.cambridge.org/core/services/aop-cambridge-core/content/view/FB2CAC644C697FEF1092C285D784CAB4/S2050509420000262a.pdf/categorical-complexity.pdf https://www.cambridge.org/core/services/aop-cambridge-core/c... Dusko Pavlovic's Monoidal computer series: 1. https://arxiv.org/pdf/1208.5205 https://arxiv.org/pdf/1208.5205 2. https://arxiv.org/pdf/1402.5687 https://arxiv.org/pdf/1402.5687 3. https://arxiv.org/pdf/1704.04882 https://arxiv.org/pdf/1704.04882
  - mhh__ 5y ago
    I mostly hope you're right, good luck. Post your thesis here when the time comes. I'm a bit of a philistine when it comes to cutting edge CS in this area so I'll leave you to it!
squid_demon 5y ago
Homotopy type theory is a mathematical foundation, like set theory, or Martin Lof's type theory. This is different from a proof assistant like Coq or Lean. In fact, Lean has a library which implements part of HoTT (see https://github.com/leanprover/lean2/blob/master/hott/hott.md https://github.com/leanprover/lean2/blob/master/hott/hott.md). In short, there is no comparison between Lean and HoTT.

deleted 5y ago

[deleted]

mhh__ 5y ago

I am kind of sceptical of these verified-mathematics projects in the sense that my litmus is whether I could easily verify my workings rather than the proofs I rely upon, but nonetheless I have enormous respect for those doing this work and really hope it comes to fruition. I really hope this work trickles down to our programming - state machine problems are basically "solved" (for my needs at least), but more complex programs are really hard to prove.

pramodbiligiri 5y ago
When you say that state machine problems are basically solved, are you referring to any tools that you're using to reason about them?
- mhh__ 5y ago
  By solved I really mean "in commercial use", there's probably a lot of research let to be done, but people are already verifying TLA+ specs all day everyday.
jkhdigital 5y ago
I'm a PhD student in computer science, and after spending some time on this subject I'm pretty well convinced that parts of mathematics and CS are converging towards a more unified foundational framework that will benefit both fields tremendously. In a nutshell, the key challenge is taking the core of complexity theory (which is easy to formalize in terms of state machines) and migrating it into the language(s) of category/type theory (which is much more modular/compositional). A couple interesting recent works in this area: Categorical Complexity: https://www.cambridge.org/core/services/aop-cambridge-core/content/view/FB2CAC644C697FEF1092C285D784CAB4/S2050509420000262a.pdf/categorical-complexity.pdf https://www.cambridge.org/core/services/aop-cambridge-core/c... Dusko Pavlovic's Monoidal computer series: 1. https://arxiv.org/pdf/1208.5205 https://arxiv.org/pdf/1208.5205 2. https://arxiv.org/pdf/1402.5687 https://arxiv.org/pdf/1402.5687 3. https://arxiv.org/pdf/1704.04882 https://arxiv.org/pdf/1704.04882
- mhh__ 5y ago
  I mostly hope you're right, good luck. Post your thesis here when the time comes. I'm a bit of a philistine when it comes to cutting edge CS in this area so I'll leave you to it!

squid_demon 5y ago

Homotopy type theory is a mathematical foundation, like set theory, or Martin Lof's type theory. This is different from a proof assistant like Coq or Lean. In fact, Lean has a library which implements part of HoTT (see https://github.com/leanprover/lean2/blob/master/hott/hott.md https://github.com/leanprover/lean2/blob/master/hott/hott.md). In short, there is no comparison between Lean and HoTT.