λ計算が数学的に正当化されてないというような話はしてなくて、
現実のプログラムをλ計算に反映させようと思っても入出力とか非決定計算の部分は表現しきれない
そのλ計算からはみ出す部分をどう正当化させようかという話。