David A Fisher is the founder and chief technologist at Reasoning Technology LLC and emeritus professor at Carnegie Mellon University (CMU). He has a Ph.D. in computer science from CMU, M.S.E from Moore School of Electrical Engineering at Univ. of Pennsylvania, and B.S. in mathematics from CMU. He was chief engineer for the CREATE high performance computing program within the Office of the Secretary of Defense, president of Incremental Systems Corporation, vice president for advanced development at Western Digital Corp (WDC), a program manager at National Institute of Standards and Technology (NIST), and a researcher at the Software Engineering Institute (SEI) . He has over 200 publications in programming language design, compiler construction, infrastructure protection and network security, bounded workspace and near linear time algorithms, embedded systems, theory of emergence, instruction set architectures, and high-performance computing. [ He lectures in the U.S., Canada, and Europe.].
Email: dafisher@ieee.org
DVP term expires December 2024
Presentations
Why Software Fails and Why AI cannot Help
It was once widely believed that computers would enhance the speed, reliability, and applicability of human deductive reasoning in the physical and social sciences, much as motorized vehicles (e.g., cars, trains, airplanes) have enhanced the speed, reliability, and applicability of human manual abilities in transportation. Yet, 60 years later, computers can be used confidently only for paperwork tasks, analysis of regularly structured data, and simple process control applications. Complex software rarely satisfies user needs, is untrustworthy and difficult to maintain, and largely opaque to its users. Artificial intelligence (AI) methods including heuristics, machine learning, and statistical methods are in opposition to sound deductive reasoning. This presentation explains certain practical and logical impediments to computer enhancement of human deductive reasoning, the deductive limitations of modern programming languages, the role of AI, and provides some promising alternatives.
Omega — A Declarative Programming Language
Omega is a truly declarative programming language that overcomes several practical and logical impediments to guarantees of valid and pertinent results for nontrivial computing applications. Its applications answer questions about physical and social domains rather than about computational models of those domains. Omega has the expressiveness and generality of natural language, a semantic foundation analogous to that of human deductive reasoning, and an implementation that combines traditional program synthesis and optimization methods with a proof engine for a sound intentional logic. Its programs often lack a translation to an equivalent imperative program. It is intended as a practical language that can be used directly by application domain specialists without expertise in computer science. This lecture explains the key objectives for Omega. It illustrates the problems being solved and describes the crucial technology that enable solutions while focusing on the look and feel of the language for a user perspective.
PBT – A Sound Deductive Logic for Computing
Traditional computers and programming languages are based on first-order predicate calculus which is subject to inconsistencies that cannot be discovered within the system (e.g., as shown by Russell’s paradox) and cannot guarantee valid results for nontrivial domains (e.g. as shown by Gödel’s incompleteness theorems). Traditional programming languages lack the expressive power to accurately characterize physical and social domains and to differentiate between what is and is not known. This presentation discusses the logic of property-based types (PBT) as an alternative mathematical foundation for computing. Types are similar to concepts of the mind and unlike programming language types or O-O classes.
PBT Logic is a specialized multi-order logic that precludes paradoxes, an incomplete logic that is valid for Gödel incomplete domains, and a logic that proves consistency rather than truth. It retains a law-of-the-excluded-middle in which every type/concept is either consistent or inconsistent, indirect proofs are valid, and the logic is monotonic. As an intensional logic, meaning is inherent in the relationships among its types and thus allows interoperation among separately developed applications. A PBT proof require only O( N ln N) execution time because it assumes incompleteness, directly prove only consistency, and the logic is monotonic.
