Comment by da39a3ee

> Judging by how most people write code today, I find this idea terrifying.

Writing code is not a single activity, it is a modern means of communication and information transmission. Code is written for a vast range of purposes, some better suited to less rigorous programmers than others. No-one is asking or expecting the authors of bad code that you have in mind to formalize legal systems. The latter task will be on the rigorous side of programming, presumably leaning heavily on static type checking / automated theorem proving.