Stephanie Weirich, ENIAC President’s Distinguished Professor in Computer and Information Science, aims to make software systems more reliable, maintainable, and secure. Her research improves tools that help programmers to determine the correctness of their code, which is applicable to a broad scope of software. Specifically, Weirich researches and improves Haskell, a programming language that places a lot of emphasis on correctness, thanks to its basis in logic and mathematical theories.
“People might not realize how much computational power underlies our society,” Weirich says. “Cars, for example, possess very strong correctness requirements as they have become so reliant on computation. If banks mess up their code, it can cause disaster for our financial systems. The security and correctness of these programs is very important.”
Programs for embedded systems, like those found in cars, are typically written in a programming language called “C.” Programmers make sure that their software will use data correctly by combining relevant variables into classifications known as “data types.” Types are what allow a programmer to assign rules to all of the different components of a computer program.
Weirich focuses on Haskell because she uses it to improve the type system of the language itself, which leads to even more extensive correctness for programmers. She’s making the types more expressive, and as a result, programmers can make better use of the type system to help them develop correct code.
While these tools and systems are not directly usable across different languages, the ideas are.
Read more at Penn Engineering.
