Verified Effectful Programming in F* - Catalin Hritcu
I noticed that not many people in the formal methods world have even heard of F Star. From what I’m told, it goes even further than Agda and Coq in proving correctness. I’d like to understand why if someone would explain.
View original on infosec.pub
No replies yet