Proving code equivalence

Development Compiler
1

I have been thinking about this problem for a very long time.

Can the compiler prove that two pieces of code are syntactically or semantically equivalent?

For example, can we say that the following versions of some code are equivalent?

// Some.swift

struct Bar {
   let value : Int
}

func transform (bar: Bar ) -> Foo {
   return Foo (code: bar.value)
}

struct Foo {
   let code : Int
}

// Some.swift

func transform (bar: Bar ) -> Foo {
   return Foo (code: bar.value)
}

struct Foo {
   let code : Int
}

struct Bar {
   let value : Int
}

// Some.swift

struct Foo {
   let code : Int
}

struct Bar {
   let value : Int
}

func foo (from bar: Bar ) -> Foo {
   return Foo (code: bar.value)
}
2

Determining whether two programs/functions behave the same under all inputs turns out to be equivalent to the halting problem, and therefore is undecidable in the fully general case. There are some tractable subsets of the problem though. I didn’t read it closely but the discussion in the answers here looks pretty good: computability - How do you check if two algorithms return the same result for any input? - Computer Science Stack Exchange

8 Likes