coq je samo "kako matematicar vidi resenje tog problema" naravno kroz
svoje matematicarske naocare - ko ima cekic njemu sve ekser.
asn1 jezicki moze da odradi i sve sto moze coq, pitanje je sad
okruzenja, ko/sta ce daj kod posle da procita i sta sa njim radi, coq
ima tu ideju da njegov env radi proveru dokaza i slicno, ali to je sad
externi env, nema veze sa samim jezikom.. jezicki nema nista vise od
asn1 ... asn1 je opet generalno "telekomunikaciono" okrenut (za
transmisiju, enkripciju i slicno) .. te sav njegov env gadja tu pricu ..
ali to je opet env, sam jezik moze da opise sta oces :D ...
no tih raznih "high order abstract syntax" ima dosta, sreo sam bar 10
standardizovanih ili polustandardizovanih sa donekle uradjenim env. koji
radi ovo i ono .. sve se to na kraju svede na "ja sam napravio zato sto
mi treba za X i koristim za X" i onda jos po neko to iskoristi za X i to
je to .. i vrlo je jednostavan razlog - sintaksa je generalno pdim,
kakvu god sintaksu oces to se lako napravi i isparsira .. ono "posle" je
ono sto predstavlja ozbiljan problem, a to posle da napravis
"univerzalno" ... nije jednostavno, a postavlja se pitanje dal za to
uopste ima potrebe