← Back to context

Comment by dividedbyzero

5 years ago

Everyone who thinks law-as-code on actual, not tax-code-algorithm law is a great idea: We as an industry have yet to figure out how to reliably get simple business processes into code without mishaps, imagine the hubris of attempting to get all of society into code without terrible results ...

The Dutch Tax Administration have been using controlled natural language for the specification of their legislation for some time now with JetBrains MPS (external) DSLs: https://www.youtube.com/watch?v=1pfABlzO2Wc&index=2&t=0s&lis...

They're not aiming at all of society. Parts of the law are already algorithms (not all of it), they just happen to be written in an obscure uncompilable Legalese.

This isn't python or JavaScript. This language is specifically designed to integrate with proof assistants, like ambitious hyper-secure TLS implementations or formally verified microkernels.