Maybe a mixture of TLC with Pcal may be a good beginning on a very simple algorithm (for instancethe generation of the addition table).