3 ms·

What's really needed is a language specifically written for the job. C was built for writing system software. English was built for writing poetry. Neither are

• JabavuAdams 17y ago
  I remember reading some sci-fi involving a treaty so complicated it had to be machine-verified. Too bad about that Gödel guy, though.
• cabalamat 17y ago
  Something a bit like Prolog might do the job. There would also have to be terminal predicates coded in English. So theft (in English law defined as: "dishonestly appropriat[ing] property belonging to another with the intention of permanently depriving the other of it") might be: (define ([Person]X is-thief of: [Property]P belonging-to: [Person]Y) (and (X appropriates P) (X != Y) (X intends ((Time>now) implies not (Y has P))) (dishonestly))) (define dishonestly "this is purposely left undefined in the law") (define ([Person]X appropriates [Property]P) "X does some action causing him to have control over P") There could then be a compiler and other software to automatically reason about such statements.