We propose an approach to reconcile formal methods and computational reflection. First, we introduce a formalism to study implementations, with which we express some of their desirable properties, notably one we dub *observability*. Next,we derive a protocol for first-class implementations, that enables zooming up and down the abstraction levels of a computation *at runtime*. Then we show how this unifies discussion of previously disparate techniques (from static analysis to AOP) and even trivializes some difficult ones (like live code migration). Finally, we envision how our proposed first-class semantic virtualization enables a new software architecture.

A version of this work has been submitted to SNAPL 2017: 
< https://github.com/fare/fci2017 >. 

I made a presentation on these ideas at BostonHaskell in 2016 
< https://youtu.be/heU8NyX5Hus > 
< http://fare.tunes.org/files/cs/fci-bh2016.pdf >. 

This presentation is an executive summary of my resurrected thesis on this topic (in progress): 
< http://fare.tunes.org/tmp/phd/thesis.pdf > 

These ideas are based on my work with the Tunes project in the 1990s: 
< http://tunes.org/ >. 

Bio: 

Faré is a cybernetician specialized in software growth infrastructure and currently living in NYC, and working at a large hedge fund in Connecticut. 

He is known as a Common Lisper for promoting Lisp as a scripting language <http://fare.livejournal.com/184127.html >, and having developed the build system ASDF3 < https://github.com/fare/asdf3-2013/ > and the Lisp Interface Library < https://github.com/fare/lil-ilc2012 > combining ad hoc and parametric polymorphism. 

Faré likes to think in terms of computing interactions and programming processes rather than computer devices and software artifacts. He once led the TUNES Project to reinvent computing < http://tunes.org/ > and recently started a new blog on this topic Houyhnhnm Computing <https://ngnghm.github.io/ >. 
He relatedly believes in the power of storytelling < http://fare.tunes.org/computing/bal2009.pdf > and of evolutionism < http://fare.tunes.org/computing/evolutionism.html >. 

His other interests span music, fine arts, psycho-history, epistemology, and more. He also spoke or was published at several venues < http://fare.tunes.org/liberty/ >. He tweets about computing as < http://twitter.com/ngnghm > and on other topics as < http://twitter.com/fare >. You can also find him on LiveJournal <http://fare.livejournal.com/ > and Facebook <https://facebook.com/fahree >. Finally he maintains a collection of quips < http://fare.tunes.org/fortunes/fare >.