It does. But maybe someone should prove (in Lean?) that the lack of flow control is sufficient.
Without a constraint that values aren’t ignored, the lack of flow control is certainly not sufficient, so trying to do this right would require defining (in Lean!) what an expression is.
Without a constraint that values aren’t ignored, the lack of flow control is certainly not sufficient, so trying to do this right would require defining (in Lean!) what an expression is.