Though the idea on specs vs proof systems is good enough , one of the reasons type systems are being studied is to actually make programming languages themselv

Though the idea on specs vs proof systems is good enough , one of the reasons type systems are being studied is to actually make programming languages themselves a good proof system , so much so that DSLs themselves become the spec. Proof systems have their uses and then there are places where they are just too much.The best is in the mid! >> "am the creator of the TLA+ specification language." I think TLA+ is/was being used at Amazon [1] Safety with Preservation and Progress guarantees of critical systems demand design audits at a larger scale however if the scale of the program is actually quite small , things like type-systems themselves are sufficient proof of safety. Ofcourse there are cases where even typing is too much! One of the middlepaths is actually using inspection tools on code/programs as another aspect altogether. [1]:http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo...