Hey, I was at that same school. What I also liked about F* is the ACL2 feel. Compared to Coq for instance, F* feels more like "my program proves itself" than "I

Hey, I was at that same school. What I also liked about F* is the ACL2 feel. Compared to Coq for instance, F* feels more like "my program proves itself" than "I'm writing a proof of my program".