Hacker News Reader

Comment by jkhdigital | Hacker News Reader

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

View on HN

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). In short, there is no comparison between Lean and HoTT.

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.

When you say that state machine problems are basically solved, are you referring to any tools that you're using to reason about them?

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.

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

Dusko Pavlovic's Monoidal computer series: 1. https://arxiv.org/pdf/1208.5205 2. https://arxiv.org/pdf/1402.5687 3. https://arxiv.org/pdf/1704.04882

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!

Reply on news.ycombinator.com