I feel many people here miss the point: it's not edit edit edit ./src/Browser maybe annotate it with some smth ./verify some-property ./src/Browser.ml &&

I feel many people here miss the point: it's not edit edit edit ./src/Browser maybe annotate it with some smth ./verify some-property ./src/Browser.ml && echo 'seems OK, ship it!' It is coq proof.coq > ./src/Browser.ml The source code is just a side effect of proving some theorem. How long do you think it's going to take before program formal proof becomes the new standard in commercial applications quality standard? Long enough