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.

>>10
A team of EXPERT LOGICIANS could invest a large effort in creating a verification system that is proven correct with peer reviewed human-written proofs. Then once this verifier is reasonably trusted it can review other sources and produce results, so that many programmers, qualified and unqualified, will have the benefit of seeing its reports on their sources.