Wednesday, February 18, 2009

Principles of Programming Research in the Computer Science Department at Carnegie Mellon

Un extracto que me pareció interesante de la carta de presentación del centro de investigación en programación (lenguajes) de la universidad de Carnagie Mellon:

"Our success in advancing an integrated view of Computer Science encourages us to take on even greater challenges, and opens up many new possibilities for us to explore. We envision that future languages will have fully formal definitions with fully checked proofs of their safety and security properties as a matter of course. Currently available tools, such as Twelf, are already expressive enough to make this feasible for realistic languages such as the POPLMark Challenge (posed by Pierce and others at UPenn) and large fragments of the ML language. Research is already under way on enriching their expressive power and convenience to make the task simpler, more modular, and easier to maintain and evolve. In particular we envision the development of logical frameworks that support a more direct and natural representation of shared state and of concurrent interaction than is currently feasible.

Our experience with the design and implementation of certifying compilers emboldens us to assert that in the future all compilers will be certifying compilers that will make use of expressive type systems in intermediate and object code, as well as source languages. Compilers are very complex software systems that are notoriously difficult to maintain and evolve. Certification permits a degree of self-checking within a compiler that greatly increases the modularity of the compiler itself, and correspondingly vastly enhances our ability to make significant changes to a component without disrupting crucial invariants assumed by other components. Moreover, certifying compilers generate object code that carries with it a machine-checkable proof of safety and security properties, eliminating or greatly reducing the need to rely on the correctness of a compiler to ensure the well-behavior of a binary executable.

The effectiveness of type systems for improving code quality, reducing development costs, and enhancing maintainability of software is by now beyond dispute. We believe that the trend toward languages with increasingly expressive type systems will accelerate, and that the demands for type systems of ever-greater expressive power will increase as developers become accustomed to their use. In the near future we expect to see type systems that are capable of expressing, and mechanically enforcing, crucial data structure and protocol invariants across module boundaries. In the longer term we expect a convergence of type systems and specification languages to achieve a complete integration of these important tools for reasoning about program behavior. There is every reason to pursue these goals aggressively, and we are optimistic that the foundation of tools and theories that we have developed will serve as a solid basis for this work.

Speaking more broadly, we believe that it is time to challenge the prevalent, if tacit, assumption that we must live with low-quality, unreliable software that is prohibitively expensive to improve, much less replace. Rather than accept the status quo and try to live with it, we do better to challenge it and try to do better. It is our contention that a comprehensive approach based on the application of fundamental theory to programming practice is the best strategy for overcoming the limitations of current software systems and practices."

Link: http://www.csd.cs.cmu.edu/research/areas/principleprogr/