Does total functional programming not do it for you as a middle ground? In particular look at Dhall and its theoretical properties, but there are more possibili

Does total functional programming not do it for you as a middle ground? In particular look at Dhall and its theoretical properties, but there are more possibilities where that came from. There are a lot of typed lambda calculi with various normalizing properties, which I believe can be read as nice analyzability, halting but still somewhat expressive.