For most of us, the language of computer software seems removed from daily life, far from our routines of morning coffee and email check.
We’re only reminded of it when glitches in software programs create havoc — maybe in the form of a power outage (what — no coffee?) or annoying, erratic computer updates (mostly because we keep choosing ‘remind me later’).
All those little pop-up fixes we receive are discovered after the software has been released and it isn’t working quite right.
Through Denison’s Summer Scholars Program, Sihan Cai ’20, a computer science major and international student from China, spent part of his 2018 summer at Clemson University helping to find a solution to this issue. Two Denison alumni and Emerita Professor Joan Krone joined Cai in the work. Krone, whose field is mathematics and computer science, has been working to solve this nest of thorns literally for decades.
The usual approach to figuring out whether or not software is going to work is through testing. Just try it out. But even if a program works flawlessly on all test runs, things can still go wrong. It’s an ongoing problem that plagues the field of software engineering.
“It’s very difficult when you write a program in any software language to prove it’s correct,” explains Krone. “You can try it a million times and still not be absolutely certain that every possibility has been tested.”
So, more than 20 years ago, Krone wanted to find a way to use mathematics to prove the correctness of programs, rather than just relying on testing. She began working with Murali Sitaraman, a Clemson University professor whom she met in graduate school, along with other collaborators to design a software language called ReSoLVE (Reusable Software Language with Verification and Efficiency).
“It is a real delight to see a student making such great strides toward new technology”
The goal is to write the mathematical equivalent of what the program does. In a nutshell, ReSoLVE uses standard mathematical logic to create an accompanying proof for each software command. Over the course of the program, the lines are replaced completely with a mathematical statement and if you can prove that mathematical statement, the program is correct.
“We have designed and evolved this language,” Krone says. “It is an academic language right now and is used at several universities to teach software engineering from a mathematical point of view. It’s not a commercial language at this point, though that is the goal. There’s still a long way to go.”
Krone has had help from several Denison students over the years. Cai became familiar with the ReSoLVE language during his early experience scholars project his sophomore summer. For the summer 2018 project, he worked with two of her former students, Dan Welch ’13 and YuShan Sun ’10, who are now working on Ph.D. degrees at Clemson.
Cai created a tutorial on the ReSoLVE compiler system, which is the program that takes a high-level language like ReSoLVE and translates it into machine code so it will run on a computer.
“It is a real delight to see a student making such great strides toward new technology, toward new ideas, toward solving some of the serious problems that exist in technology,” Krone says.
“Sihan has such a great work ethic. He’s not only capable but he’s also just a nice person. One of the things I see among our students, and Sihan in particular, is he is always willing to help someone else.”
She adds, “As we look at the news, it sometimes seems like the world is falling apart, but when I see these wonderful students with such great ideas and such great ability, that gives me a sense of optimism.”
