Here's a place for the Program Languages, Type Theory and Logic research with an attempt to elaborate the best target language for a program generation and abstractions extraction by an AGI system.