DSR enhanced security and "formal verification" course
Here we are quickly going through the rabbithole of thoughts that caused so much pain to almost all software language and compiler architects over the last decades.
- TLA+ - the T stands for "Temporal Logic"
- Thinking about your ***free time*** in SQL
- Fun example: Rabbit and Elephant in a fridge
- Moving rabbit and elephant from one fridge to the other
- Thinking about the rabbit example in TLA+
- The new Python "pattern matching" syntax
- Notation standards in math, sciences and computer sciences
TLA+ - the T stands for "Temporal Logic"
What famous Leslie Lamport's TLA+ verifier is all about: Temporal Logic:
https://www.researchgate.net/publication/373590095_Standpoint_Linear_Temporal_Logic
https://en.wikipedia.org/wiki/Allen's_interval_algebra
In fact, it's talking about Gantt Diagrams: https://www.gantt.com/ge/
Flows can be visualized with highly sophisticated Graphviz, written in pure C:
Playground: https://graphviz.org/Gallery/neato/process.html
http://magjac.com/graphviz-visual-editor/
Talking philosophically: What relation is there between this diagram and the "Rabbit - Elephant - in the fridge" example timeline? -> Go forward, come back!
Thinking about your ***free time*** in SQL
PostgreSQL on DBFiddle: https://dbfiddle.uk/lvn7uD7I
void printInts(List<int> x) => print(x);
https://www.postgresql.org/docs/current/rangetypes.html
Example: Hotel reservations and overlapping bookings
https://hashrocket.com/blog/posts/postgresql-daterange-and-efficient-time-management
Fun example: Rabbit and Elephant in a fridge
Q: How you get a rabbit into a fridge?
A: Simple: Door open, Rabbit in, Door close, in short: Do-Ri-Dc
Q: How do you get an elephant into the fridge?
A: Door open, rabbit out (because the elephant may step on the poor rabbit), elephant in: Do-Ro-Ei-Dc
Now we do it "multi threaded" on two interleaving "Gantt" timelines:
Wasn't thread-safe, obviously! Let's file a bug. How would you make it "thread safe"?
Q: What is "atomicity". What's the correspondence in SQL?
That's virtually is what Leslie Lamport's TLA+ verifier is all about and what you can learn in either Hillel's courses: https://www.dabeaz.com/tla.html or directly in Leslie Lamport's excellent TLA+ course on YouTube: https://youtube.com/@tlavideocourse8540/videos
For me as philosopher it's just one more mental model to play with. Notation of Temporal Logic is the other problem. There are almost no standards in that area.
Moving rabbit and elephant from one fridge to the other
To the free TLA+ online book: https://www.learntla.com/
So learning another language, notation, compiler, gui? Nope: You will very soon learn, that you can do it easily in any other language too! And you will learn, that you will have so simplify, to strip off many features of your beloved programming language to make things ***verifyable***. Modern languages are bloated, overloaded -feature wise.
Thinking about the rabbit example in TLA+
Q: What are the constraints in the rabbit and elephant example?
- Were they implicit or explicit?
- How do we express these constraints in TLA+?
- Can we see the fridge as bank account? How?
- How do we "withdraw" Rabbit and Elephant from the fridge?
- Where are they "deposited" if they are not in the fridge?
Q: Do you now see the parallels?
- How would you formulate the Rabbit problem in TLA+?
Q: Obviously TLA+ permutates states: process wire \in 1..NumTransfers
- What "state" can the fridge be in?
- How many processes do we / can we have?
Q: Where did the "timeline thinking" disappear to? Hasn't Leslie Lamport forgotten something?
Q: Can we permutate the processes in Rabbit example?
- How many processes are there? Let's write them all down:
- Do-Ri-Dc
- Do-Ei-Dc (here a constraint has to be set: Elephant never step on Rabbit!)
- Do-Ro-Ei-Dc (Lucky Rabbit, constrained fulfilled!)
- Do-Ro-Dc (trivial, that the Rabbit also can be taken out of the fridge?)
- Do-Eo-Dc (sure ...)
- ...
Q: Have we gotten all processes right?
- What is with time delays? State "Do" and nothing happens?
- Do we have to reformulate our problem?
State "Do" - Time starts ... - ... fridge empty ... still empty ... still empty ...
And then another process finds the Door in "state opened" and quickly puts the Elephant in? ... with "Dc" pending, time delayed ...
And then another process wants to put the Rabbit in, too? Note: Elephant is in the door, but the process was't completed, the door is not yet closed.
Q: Is the Rabbit allowed to step on the Elephant? A: Yes! Obviously no harm!
How we do formulate that as constraint? Is that constaint necessary?
Q: Do we have to insert checks for "Do" and "Dc" states?
Q: Would this solve our problem?
Q: Would adding a check for "if there is something in the fridge and who" help?
Q: What if that check is time delayed?
Q: Do we need a guard or a sentinel? (in german "Wächter")
- Another lock before the "Dc" locked door?
- Do we need two doors? Or three? Would 100 doors solve that problem?
Q: What about a ticket automat? Rabbit, Elephant need to draw a ticket first?
- What's a ticket lock? Does e.g. Rust have a ticket lock? What does the "borrow-checker" internally do?
Q: What processes are allowed when the Elephant is in the fridge?
Q: What processes are allowed when the Rabbit is in the fridge?
Q: What processes are allowed when Elephant first - and then Rabbit - then both are in the fridge?
Q: Can we make a "rules" table, which processes are allowed and when? Refering to
So a flow graph like in https://graphviz.org/Gallery/neato/process.html is not sufficient. We need conditioned flows:
Means: We need a "Transition State Table" of the form:
https://github.com/gbmhunter/FunctionPointerStateMachineExample/
Q: Before we start: Are "Do" - Door open and "Dc" - Door close states or processes? Or both?
...
...
...
Can you imagine that most programmers are confused by this?
The new Python "pattern matching" syntax
https://peps.python.org/pep-0622/
Another example:
Now we introduce guards or sentinels, TLA+ constraints
Python obviously has a built-in type verifier:
Notation standards in math, sciences and computer sciences
The complete overview of math notation on 10 pages:
http://www.tug.org/texshowcase/cheat.pdf
https://en.wikipedia.org/w/index.php?title=Glossary_of_mathematical_symbols
New Standpoint Temporal Logic notation
https://www.researchgate.net/publication/373590095_Standpoint_Linear_Temporal_Logic
What's a "standpoint"? A context. You you see the world is your context. It's how you interpret events. Like environment variables in programming, in containers, in machine code execution stacks. Nothing more!
Thinking in "timeline - events - rules (constraints)" model
These are the upcoming new patterns in computing. Why? The do scale on parallel and distributed computing!
There is a new software architecture upcoming, which has a very quite different approach of "seeing, interpreting the world": http://event-db.com
ECS: https://en.wikipedia.org/wiki/Entity_component_system
CQRS: https://en.wikipedia.org/wiki/Command-Query-Responsibility-Segregation
Event Sourcing: https://en.wikipedia.org/wiki/Command-Query-Responsibility-Segregation
Computer science metanotation (CSM)
https://cs.stackexchange.com/questions/83770/help-understand-the-notation
Guy Steele: https://youtube.com/watch?v=7HKbjYqqPPQ
https://youtube.com/watch?v=dCuZkaaou0Q&t=1h1m0s
Back to last lesson - https://rentry.co/DSRsecuritycoursepart8 Next lesson: https://rentry.co/DSRsecuritycoursepart10