What fragment of Lean is at least weakly normalizing?

Stream: lean4

[nrs]

Am interested in using Lean as a correct-by-construction general programming language, and I've read in the article about Lean4Lean that it fails to be strongly normalizing. Do we know what fragments are at least weakly normalizing?

[Mario Carneiro]

if you exclude Acc and never reduce proofs it's plausible that the resulting system is strongly normalizing

[Patrick Massot]

I’m not an expert in those question but I guess the two parts of your first sentence are completely unrelated. The strong normalization property does not prevent Lean from doing correct by construction programming.