lets-prove-leftpad icon indicating copy to clipboard operation
lets-prove-leftpad copied to clipboard

Add summary statistics about different proofs

Open solna86 opened this issue 4 years ago • 0 comments

I found this repository incredibly interesting.

I think it would be very informative to extract some kind of naive summary statistics (e.g. LOC) to understand the compromises between different proof systems.

As an old user of Spec#, Dafny's precursor, I was pleasantly surprised to see how well Dafny and other systems (e.g. Lean, Agda, F*, Coq/SSReflect or Idris) compare to Isabelle or Liquid Haskell.

solna86 avatar Oct 02 '21 19:10 solna86