The nice thing is that you can actually build stuff like web servers in a total language :)
Using something called co-induction a total language can model things that are potentially infinite, e.g. a web server. Co-induction replaces the requirement that every function must terminate with the requirement that the next step (e.g. the next value of a stream) can be calculated in finite time. So, the event loop could be modelled using co-induction as long as long as the event handlers do not contain infinite loops.
The style of coinductive reasoning is very different.
In general, in induction, one has a base case and an inductive case. Hence, you can only build "finite" objects (since you start with the base case and you can apply the induction rule a finite number of times)
In coinduction, you start with an infinite object, and you show that you can "progress" - that is, take a step in your computation. So, this shows that you can _reach_ states in finite time, even if the full structure is inaccessible, since you show progress on each state.
The phrase that I've heard is "induction is to prove what's true, coinduction is to prove what's not false"
Please do Google "practical coinduction" it has a wealth of examples.
