|
|
|
|
|
|
by deterministic
121 days ago
|
|
|
Completely agree. Refinement types is a much more practical tool for software developers focusing on writing real world correct code. Using LEAN or Coq requires you to basically convert your code to LEAN/Coq before you can start proving anything. And importing some complicated Hoare logic library. While proving things correct in Dafny (for example) feels much more like programming. |
|
|