MINDLESS C0DING

https://github.com/jonleivent/mindless-coding

Specifications, such as the dependently-typed inductive definitions of avltree and rbtree, and the dependently-typed arguments and results of their functions, are made sufficiently complete so as to constrain any implementation that type-checks to be fully correct. For example, the avltree and rbtree types both include a contents index that constrains each tree to contain exactly the specified contents in exactly the specified (sorted) order. Performance-related properties are not included - but this might be pursued in the future.

>>7
Automated verification only takes the time out of things. You need smart superior people building things and not just anybody. A retard making an automated verification system is going to make that system be fundamentally insecure.