Hello! Andy Wingo <wi...@pobox.com> skribis:
> Anyway this second, proof side of types, is the side that Scheme does > not have. C has a stronger story in that regard. Right; but let’s not oversell C. ;-) Lisps are definitely closer to automated theorem provers than C. ACL2 and αleanTAP come to mind. Ludo’.
