Comment by lambdaxymox

I don't know about superoptimization, but JetBrains does have a HoTT-based language and proof assistant called Arend for doing mathematics in.