|
|
|
|
|
|
by Verdex
850 days ago
|
|
|
Ultimately, I don't think so. All the HoTT stuff seems to really be focusing on constructing proof objects so that the computer can run them on mathematics which would otherwise not have any computer verification run on it. More or less advanced type checking for math. Meanwhile, the MGS language's topological collections and associated transforms seems to be about simulating things like chemical reactions. Not really verification so much as exploration. Although, to be sure, I think both are examples of how mathematics (even highly abstract mathematics like topology) can be useful to other disciplines. |
|
|
I disagree. There's a migration from Haskell to Lean 4, which is influenced by HoTT, and is a credible general purpose programming language.
Arguably, _the_ credible general purpose programming language, if one believes that programming should feel like doing mathematics. Languages are shaped by their target tasks, and writing tactics for proofs subsumes any other task one might consider. Programming is recognizing pattern, and pattern runs deep in Lean.
When we're young, but past existential BS, we start to think that ten years of training will yield productive years that outstrip decades of muddling in ad hoc languages if we hadn't made the commitment. But soon, few want to make the commitment.
If programming is ever going to become far more advanced, it will take the form of successors to Haskell and Lean.