1

Too Many Bugs to Count

​

An Intuition into Why Formal Verification is Fundamentally Hard

​

​

​

​

​

​

​

​

​

​

​

​

​

Ali Atiia

​

Electisec Block II Retreat Session

July 24th 2022

2

Motivation:

• FAQ: will automation tools replace auditors long-term?�
• Intuition into the notions of impossibility and hardness of computational problems�

​

3

xP-Ex-

​

4

xP-Ex-

​

Take the following meaningless sentence as absolute Truth :

Hofstadter, D.R. Gödel, Escher, Bach: An Eternal Golden Braid. London: Penguin, 2000. (with modification)

5

xP-Ex-

​

Take the following meaningless sentence as absolute Truth :

It is composed of three letters: �P, E, and Hyphen (-)

​

​

6

xP-Ex-

​

Take the following meaningless sentence as absolute Truth :

It is composed of three letters: �P, E, and Hyphen (-)

x is not a letter, it is just a placeholder

for one or more Hyphens

​

7

This sentence is True … �self-evidently so … �no questions asked.

xP-Ex-

​

Take the following meaningless sentence as absolute Truth :

It is composed of three letters: �P, E, and Hyphen (-)

x is not a letter, it is just a placeholder

for one or more Hyphens

​

8

xP-Ex-

​

Take the following meaningless sentence as absolute Truth :

Obey the following rule mechanically & blindly :

If xPyEz is True,

Then xPy-Ez- is True too

​

Take the following meaningless sentence as absolute Truth :

9

Obey the following rule mechanically & blindly :

xP-Ex-

​

x,y,z stand for one or more hyphens

If xPyEz is True,

Then xPy-Ez- is True too

​

Take the following meaningless sentence as absolute Truth :

10

Obey the following rule mechanically & blindly :

xP-Ex-

​

-P-E--

​

--P-E---

​

Examples: �self-evident Truths

If xPyEz is True,

Then xPy-Ez- is True too

​

Take the following meaningless sentence as absolute Truth :

11

Obey the following rule mechanically & blindly :

xP-Ex-

​

-P-E--

​

--P-E---

​

-P--E---

​

--P--E----

​

Examples: �Truths by virtue of rule

If xPyEz is True,

Then xPy-Ez- is True too

​

Examples: �self-evident Truths

Take the following meaningless sentence as absolute Truth :

12

Obey the following rule mechanically & blindly :

xP-Ex-

​

-P-E--

​

-P--E---

​

--P-E---

​

--P--E----

​

If xPyEz is True,

Then xPy-Ez- is True too

​

Infinitely many Truths

Take the following meaningless sentence as absolute Truth :

13

Obey the following rule mechanically & blindly :

xP-Ex-

​

Infinitely many Truths

If xPyEz is True,

Then xPy-Ez- is True too

​

Take the following meaningless sentence as absolute Truth :

14

Obey the following rule mechanically & blindly :

xP-Ex-

​

?

What if we interpreted :

P as ‘plus’ and

E as ‘equals’ ?

- P – E --

​

1 + 1 = 2

If xPyEz is True,

Then xPy-Ez- is True too

​

Take the following meaningless sentence as absolute Truth :

15

Obey the following rule mechanically & blindly :

xP-Ex-

​

?

What if we interpreted :

P as ‘plus’ and

E as ‘equals’ ?

- P – E --

​

If xPyEz is True,

Then xPy-Ez- is True too

​

-P--E---

​

1 + 2 = 3

--P-E---

​

2 +1 = 3

--P--E----

​

2 + 2 = 4

1 + 1 = 2

Take the following meaningless sentence as absolute Truth :

16

Obey the following rule mechanically & blindly :

xP-Ex-

​

If xPyEz is True,

Then xPy-Ez- is True too

​

This is the (meaningful) set of all legal arithmetic additions over the set of natural numbers

Take the following meaningless sentence as absolute Truth :

17

Obey the following rule mechanically & blindly :

xP-Ex-

​

If xPyEz is True,

Then xPy-Ez- is True too

​

If we encode symbols with numbers:

P = 101

E = 110

- = 111

​

Take the following meaningless sentence as absolute Truth :

18

Obey the following rule mechanically & blindly :

xP-Ex-

​

If xPyEz is True,

Then xPy-Ez- is True too

​

P = 101

E = 110

- = 111

​

we can treat strings as numbers,

example:

-P-E-- = 111 101 111 110 111 111

= 253887 (in decimal)

If we encode symbols with numbers:

Take the following meaningless sentence as absolute Truth :

19

Obey the following rule mechanically & blindly :

xP-Ex-

​

If xPyEz is True,

Then xPy-Ez- is True too

​

Every dot here is a number which, once decoded back to P’s, E’s and hyphens, corresponds to a a self-evident or derived Truth

we can treat strings as numbers,

example:

-P-E-- = 111 101 111 110 111 111

= 253887 (in decimal)

20

The set of natural numbers N

a subset of N

21

The set of natural numbers N

a subset of N

Let’s employ a ‘bouncer’ to decide which numbers are IN and which are OUT:

22

The set of natural numbers N

a subset of N

Any machine capable of mechanically following simple unambiguous instructions would suffice, no ‘intelligence’ required

Or

Let’s employ a ‘bouncer’ to decide which numbers are IN and which are OUT:

23

The set of natural numbers N

a subset of N

Any machine capable of mechanically following simple unambiguous instructions would suffice, no ‘intelligence’ required

Let’s employ a ‘bouncer’ to decide which numbers are IN and which are OUT:

1. Take a number n as input

2. k = n in binary

3. Generate all TRUTH/TRUTH s, #digit(s) = #digits(k)� put it in container C

4. Examine every element s in C

if s = k, accept n and halt.

5. Reject n

​

​

​

24

The set of natural numbers N

The language … and the machine

a subset of N

1. Take a number n as input

2. k = n in binary

3. Generate all TRUTH/TRUTH s, #digit(s) = #digits(k)� put it in container C

4. Examine every element s in C

if s = k, accept n and halt.

5. Reject n

​

​

​

25

The set of natural numbers N

The language … and the machine

a subset of N

1. Take a number n as input

2. k = n in binary

3. Generate all TRUTH/TRUTH s, #digit(s) = #digits(k)� put it in container C

4. Examine every element s in C

if s = k, accept n and halt.

5. Reject n

​

​

​

The machine instructions are themselves written using some kind of alphabet (English-ish, Java, Python, assembly … doesn’t matter)

​

If we encode that alphabet with numbers, then the above machine is a number itself

26

The set of natural numbers N

1. Take a number n as input

2. k = n in binary

3. Generate every TRUTH/TRUTH s, #digit(s) = #digits(k)� put it in container C

4. Examine every element s in C

if s = k, accept n and halt.

5. Reject n

​

​

​

The language … and the machine

a subset of N

The machine instructions are themselves written using some kind of alphabet (English-ish, Java, Python, assembly … doesn’t matter)

​

If we encode that alphabet with numbers, then the above machine is a number itself

27

The set of natural numbers N

The language … and the machine

28

The set of natural numbers N

The language … and the machine

More languages and machines …

29

The set of natural numbers N

The language … and the machine

More languages and machines …

The English language (i.e. an infinite set of numbers each encoding one of the infinitely-many syntactically-correct English sentences)

30

The set of natural numbers N

The language … and the machine

More languages and machines …

The English language (i.e. an infinite set of numbers each encoding one of the infinitely-many syntactically-correct English sentences)

a parser written in Java (more precisely, the number encoding for that parser’s code)

31

The set of natural numbers N

The language … and the machine

More languages and machines …

All DNA sequences encoding for valid Panda genomes

32

The set of natural numbers N

The language … and the machine

More languages and machines …

All DNA sequences encoding for valid Panda genomes

A number encoding bio-specs of female Panda womb (or encoding the software program simulating it)

33

The set of natural numbers N

The language … and the machine

More languages and machines …

Prime numbers (or the numbers encoding those numbers!)

34

The set of natural numbers N

The language … and the machine

More languages and machines …

Primality-testing algorithm (or the software implementation of that algorithm (more precisely: the number encoding that implementation … yadda .. yadda))

Prime numbers (or the numbers encoding those numbers!)

35

The set of natural numbers N

The language … and the machine

More languages and machines …

an infinite set of numbers each encoding a triplet (a, b, c) where c is the Greatest Common Divisor of a and b

36

The set of natural numbers N

The language … and the machine

More languages and machines …

Euclid’s method for finding greatest common divisor

an infinite set of numbers each encoding a triplet (a, b, c) where c is the Greatest Common Divisor of a and b

37

Languages

Machines

38

Languages

Machines

TRUTHS

PROOFS

39

40

Is there a SUPER-language ? A language of all languages ?

41

Is there a SUPER-language ? A language of all languages ?

In other words …

​

If we started off with a more sophisticated set of alphabet like :

∀ ∃ ∄ { } | ∩ ∪ ⊆ ⊂ ⊄ ⊇ ⊃ ⊅ \ ∈ ∉ × Ø % ⇒ ¬

plus the Greek alphabet as placeholders of objects etc

42

Is there a SUPER-language ? A language of all languages ?

And accepted few self-evident Truths (axioms)

In other words …

​

If we started off with a more sophisticated set of alphabet like :

∀ ∃ ∄ { } | ∩ ∪ ⊆ ⊂ ⊄ ⊇ ⊃ ⊅ \ ∈ ∉ × Ø % ⇒ ¬

plus the Greek alphabet as placeholders of objects etc

43

Is there a SUPER-language ? A language of all languages ?

Is there a guarantee that every conceivable language (hence every Truth) is inside this SUPER-language ?

In other words …

​

If we started off with a more sophisticated set of alphabet like :

And accepted few self-evident Truths (axioms)

∀ ∃ ∄ { } | ∩ ∪ ⊆ ⊂ ⊄ ⊇ ⊃ ⊅ \ ∈ ∉ × Ø % ⇒ ¬

plus the Greek alphabet as placeholders of objects etc

44

Is there a SUPER-language ? A language of all languages ?

45

Is there a SUPER-language ? A language of all languages ?

Is there a SUPER-machine ? A bouncer machine for SUPER-language ?

46

Is there a SUPER-language ? A language of all languages ?

Is there a SUPER-machine ? A bouncer machine for SUPER-language ?

SUPER-machine = aware of the axioms of SUPER-language

faithful to the rules of SUPER-language

​

47

Is there a SUPER-language ? A language of all languages ?

Is there a SUPER-machine ? A bouncer machine for SUPER-language ?

Nothing SUPER about this machine really, when consulted about whether a number is IN our OUT, it consults the axioms and applies the rules mechanically

​

e.g. recall the machine sketched above for the P-E language has no conception of “addition”

SUPER-machine = aware of the axioms of SUPER-language

faithful to the rules of SUPER-language

​

48

Is there a SUPER-language ?

Is there a SUPER-machine ?

Suppose someone clever constructed a SUPER-language L

(s/he chose an alphabet, declared some axioms, and defined the rules of derivation)

49

Supposedly L contains all Truths about anything:

Numbers ………………………...….arithmetic etc

Cities, People ………………………….. graphs etc

DNA Sequences ……………….. alignments etc

P-E system …………………….........……addition

.

.

objects …………………………….relations

​

Is there a SUPER-language ?

Is there a SUPER-machine ?

Suppose someone clever constructed a SUPER-language L

(s/he chose an alphabet, declared some axioms, and defined the rules of derivation)

50

Supposedly L contains all Truths about anything:

Numbers ………………………...….arithmetic etc

Cities, People ………………………….. graphs etc

DNA Sequences ……………….. alignments etc

P-E system …………………….........……addition

.

.

objects …………………………….relations

​

Take this to your wildest most abstract imagination

Is there a SUPER-language ?

Is there a SUPER-machine ?

Suppose someone clever constructed a SUPER-language L

(s/he chose an alphabet, declared some axioms, and defined the rules of derivation)

51

Supposedly L contains all truths about anything:

So consider this statement which should be in L :

G = “G is not a Truth in L”

Is there a SUPER-language ?

Is there a SUPER-machine ?

52

G = “G is not a Truth in L”

If L said G is True, it would have effectively shot itself in the foot and proven its own inconsistency !

​

Why ?

Is there a SUPER-language ?

Is there a SUPER-machine ?

Supposedly L contains all truths about anything:

So consider this statement which should be in L :

53

G = “G is not a Truth in L”

If L said G is True, it would have effectively shot itself in the foot and proven its own inconsistency !

​

Why ? Because both G and NOT(G) would be True … ops!

​

Is there a SUPER-language ?

Is there a SUPER-machine ?

Supposedly L contains all truths about anything:

So consider this statement which should be in L :

Logical blackhole (!)

54

Socrates: “All Greeks are liars”

G is basically the Liar’s Paradox stated mathematically :

55

Socrates: “All Greeks are liars”

Neither True nor False … but something weird in between

G is basically the Liar’s Paradox stated mathematically :

56

“For any universal record player, realized or yet to be, there exists a record which, if played, will result in the player’s indirect self-destruction.”

Hofstadter, D.R. Gödel, Escher, Bach: An Eternal Golden Braid. London: Penguin, 2000. (with modification)

A metaphor ..

57

No

Some Truths are beyond provability

Is there a SUPER-machine ?

Is there a SUPER-language ?

58

Is there a SUPER-machine ?

Is there a SUPER-language ?

59

Is there a SUPER-machine ?

Is there a SUPER-language ?

Let’s settle for a super-language (small letter ‘s’) ..

(ignore those logical blackholes, when was the last time someone bumped into one anyway, practically speaking ? )

60

super-language = all Truths (minus some weird “problematic statements”)

​

Is there a SUPER-machine ?

Is there a SUPER-language ?

Let’s settle for a super-language (in small letters) ..

61

super-language = all Truths (minus some weird “problematic statements”)

​

super-language can describe everything, including machines

Is there a SUPER-machine ?

Is there a SUPER-language ?

Let’s settle for a super-language (in small letters) ..

62

Every conceivable sentence

Every conceivable machine

∞

∞

Is there a SUPER-machine ?

Is there a SUPER-language ?

63