http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/ is a good way to learn coq if you are interested and don't already know it. also,

http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/ is a good way to learn coq if you are interested and don't already know it. also, i didn't completely follow the final example, but you might find that category theory is relevant. related, it's not completely clear to me why you're not happy with functional programming. in a sense what academic functional programmers are doing is what you want your software to do. they're just not smart enough to put it in a compiler yet. i think. for example http://www.fing.edu.uy/inco/cursos/proggen/Articulos/sorting.ps.gz http://www.fing.edu.uy/inco/cursos/proggen/Articulos/sorting... (isn't that kinda what you want?)