> Heterogeneity belongs in the type system, not in the runtime.

Is the intent that applications developed with this are compiled for target hardware on a machine-specific basis?

e.g. I define a machine file for my i5 and GTX3080, and another machine file for my gnarly datacenter rack, and the compiler compiles specifically for each?

That way the same source file is "provable" for different hardware configurations without relying on a runtime to be identicallu implemented?