[thesz]

The article mentions the inability to decide equality of functions. A paper [1] about proving properties of functional programs shows how to do that modulo halting theorem. E.g., if (\x -> f x == g x) halts we can decide whether f and g are equal.

[1] http://xenon.kiam.ru/~roman/doc/2009-Klyuchnikov_Romanenko--...

Basically, if supercompilation of the expression above results in a huge nested case that has either True as a result (termination) or an application of function (not terminated due to infinite data structures, for example), then functions are equivalent. Otherwise, if there is at least one False, they are not, the path to False provides a counterexample.

[bmc7505]

One of the authors of this work apparently now works on supercompilers at Meta and open sourced some nice tools for equivalence checking based on graph rewriting [1] and constructive type theory [2]. If you're interested in that kind of thing I would recommend checking out his work:

[1]: https://github.com/ilya-klyuchnikov/mrsc

[2]: https://github.com/ilya-klyuchnikov/ttlite

[ajkjk]

Are we already calling it 'Meta' unironically?

[noduerme]

No one should ever call that thing Meta. We have to draw the line somewhere. Facebook needs to be gratuitously dead named.

[steego]

To be fair, people who work on supercompilers have been in the meta space long before it was ironic.

[rowanG077]

Supercompilation has also been known as metacompilation for decades.

[guerrilla]

In this case by Meta I think they mean Facebook. Name change today in case you missed thar.

[mro_name]

Whom? Metaface?