Аннотация:The Meta-PRL system combines the properties of an interactive LCF-style tactic-based proof assistant, a logical framework, a logical programming environment, and a formal methods programming toolkit. This paper provides an overview of the system focusing on the features that did not exist in the previous generations of PRL systems.