🚀 go-pugleaf

Hi net,


Let us consider a circular list. It can be defined by an ML-like data
type such as

	list 'a = nil | cons of 'a * list 'a ;

and the assertion:

	The last element for the list is the first one.

Does anyone know of programming systems in which such assertions can be
expressed formally and used at either run-time or compile-time?  I know
of Ait Kaci's LIFE which is mainly restricted to local structure
constraints.  

Thanks in advance,
Philippe Bazet.
e-mail: bazet@cri.ensmp.fr