Golang GC is mostly concurrent, not stop-the-world. There's a tiny STW pause at the end of the 'mark' phase that could in principle be avoided, but it's not a huge issue wrt. performance.

SAT is a standard GOFAI problem and you can of course use any programming language in the ML family to write a SAT solver. Thus I'd say that "ML/AI" approaches are, if anything, quite applicable!

> solvers are just a large ensemble of heuristics for very specific sub-problems

Isn't that statement trivially applicable to anything NP-Hard (which ILP is, since it's equivalent to SAT)?

Thanks for the reference! That take of his sounds a bit confused in-context (univalence and constructivism are not directly related, you can work non-constructively and still use the overall featureset of HoTT/univalence) but then his remark about how he's just working on non-constructive stuff that we don't even know how to phrase constructively is just fair.

Relatedly, the kind of philosophical constructivism that would make claims like "non-constructive mathematics is just wrong and useless" has been a bit problematic in many ways, he's not totally off-base about this.

I disliked his skepticism about proofs-as-programs the most, but that's because I think "a direct proof is a program" is very much a worthwhile statement. Of course some mathematicians will opt not to care about that.

> but of course it's not the kind of "step forward" with immediate, observable results.

Nice, it looks like you agree with Kevin Buzzard's claim about HoTT in the presentation I linked above. While mathematicians as a whole have historically not cared all that much about the practicality of formal foundations, it's worth noting that Kevin Buzzard has quite some expertise in dealing with the Grothendieck-style fuzzy, informal reasoning about equality that happens to be a key motivation behind HoTT itself and the univalence approach. What he seems to claim on the topic is that HoTT makes it a tiny bit easier to phrase a formal treatment of these issues, but you still have to do all the really hard work of proving that everything "respects" the equalities you claim it respects. The fact that you can then "transport" mathematical objects, proofs etc. along equalities is nifty but is also the kind of thing that would be glossed over to begin with in any informal treatment, so there's no real gain wrt. that.