Migrating Android Applications to the HarmonyOS NEXT Ecosystem Using Formal Specifications

It is not a trivial task to fully automatically migrate an Android app to HarmonyOS NEXT: the platforms differ too much in architecture. I will show how it is possible to transpile Kotlin and Jetpack Compose into ArkTS and ArkUI using SMT solvers, and explain why it is still important for an engineer to understand mathematics in the era of AI.