Constructive finiteness