Thread by @mengwong

During walk&talk with CS intern yesterday: "what is stepwise refinement?"

Great question!

It offers an opportunity to relate specification languages and implementation languages, and hence to relate both to computational law.

Let me explain…

Programmers write programs in a language like Java. The program gets compiled, first to a binary suitable for the Java Virtual Machine; then the JVM executes the bytecode, converting it, ultimately, to machine code: CPU instructions.

It's not actually turtles all the way down.

In this little diagram, you start on the left, and move right.

program ––> compiler ––> bytecode ––> machine code ––> CPU ––> ⚡️

But … what lies to the LEFT of "program"? Usually, lots of meetings, involving whiteboards, and whiteboard markers empty of ink. We call that phase "requirements specification". Oh, and often involving people, too, who don't know what they want: we call them "customers". Ha, ha.

If your instinct is to solve "customers don't know what they want" you get Agile.

But what if the customers actually (kinda) do know what they want?

If our instinct is to solve requirements specification, we find a history of smart people thinking hard for 50 years.

Some of those people said, "let's never run out of whiteboard marker again", which is how we got UML. Which begat BPMN and DMN and OCL. Which begat SBVR. "Let's move the whiteboard into the computer!" Lots of boxes and arrows, lots of structure.

This sort of structure attracts Semantic Web people the way demons are attracted to pentagrams. They turn up bearing RDF and OWL and RIF and KIF and SparQL.

This sort of structure also attracts the French. Remember the French? They gave us Descartes. Galois. Fermat. Pascal. They gave us Alain Colmerauer, who invented Prolog. (And they gave us Guerlain. Serge Lutens. Grasse. But that's getting into my other hobby.)

The French also gave us B. But more on that later.

First, a detour: about implementation vs specification languages.

Between imperative and declarative programming paradigms.

Have you ever been given directions in the form of "turn left at the McDonalds, then third right, then go 600 feet and look for parking"?

And have you ever responded with, "just give me the address, I'll figure it out"?

That's the difference between imperative and declarative.

The thinking goes, it should be up to us humans to specify what we want, declaratively; and the computer should figure out the rest.

"Alexa, it looks like we're out of detergent".

A box shows up at your door three hours later.

declarative specification ––> refinement ––> imperative program

en.wikipedia.org/wiki/Refinemen…

Prolog is all about declarative. Give Prolog some facts and rules. Ask a question. Prolog, not you, figures out how to answer it.

Remember knights and knaves? Knights tell the truth; knaves lie.

All you have to do is set up the puzzle; Prolog will solve it for you.

You meet 3 inhabitants. A says: "All of us are knaves." B says: "Exactly one of us is a knight."

?- sat(A =:= (~A * ~B * ~C)), sat(B =:= card([1],[A,B,C])).
A = C, C = 0,
B = 1.

Boom.

metalevel.at/prolog/puzzles

Working with declarative, specification languages feels like a secret superpower. My language is Higher-level Than Thou.

Have you seen Ready Player One? [spoiler]

Everybody else drives forward. They crash and burn.

You hit reverse and find the secret short-cut to the prize.

Don't go forward. Go back.

Life is too short to write assembly language. So let's write programs in C.

But life is too short to write C. So let's write in Javascript and Python.

Guess what? Life is too short to write Javascript and Python!

So we should … write in … what?

If you're French, you write in B.

To get the joke, you need to know that C is the classic implementation language. Millions have suffered it. Most of the world's running programs were written in C; if they weren't, their compilers were.

What is B? B comes before C!

Go left!

B's formal methods have been used to verify automated train systems in France and NASA spacecraft in flight. clearsy.com/en/our-tools/a…

Galois would have approved. His life was definitely too short. Galois before his 21st birthday, in a duel.

It may not sound glamorous, but mathematically proving safety properties of train systems is important …

clearsy.com/en/systems-and…

Because not doing that is how you end up with dozens dead and injured.

What does this have to do with computational law? Well, the thing about legislation is that you can't "fail fast". You can't "move fast and break things." Laws are specifications, albeit informal. Computational law includes attempts to redefine them formally.

That's why controlled natural languages are interesting. They bridge the gap between natural language and formal specification. Check out Attempto Controlled English, and AceRules. attempto.ifi.uzh.ch/site/resources/

Once we REDEFINE laws as formal specifications, we can REFINE them to working code.

Until recently, the standard approach in AI was for a domain expert to buddy up with a techie to do "knowledge transfer". We call it "interpretive implementation."

We could automate some of that. The computer could automatically extract the specification from normative text. mirelproject.eu

Or we could write rules-as-code, "born digital", from scratch.

That's the REDEFINE step.

However it was born, we can REFINE machine-consumable specification into useful tools.

Natural language generation offers backward-compatibility with lawmaking.

Static analysis offers unit testing, model checking, and more. cse.chalmers.se/~gersch/slides…

Tnx for coming to my TEDtalk