Proofs and development

[Alan Grover]

At 10:04 AM -0500 6/2/98, Marko van Eekelen wrote:
>I hope this gives you an idea of what is going on in our group concerning
>automatic reasoning about programs.

Yes! Yes! I think we need these sorts of tools to improve the quality of
software. Everyone is always saying "get it right before worrying about
performance", but there is little to support that activity.

I can also see that some theorem proving could be useful to the compiler,
leading to optimizations (Reverse(Reverse x) = x). Perhaps leading to a
next generation language where we don't have to solve the left side of
functions before we write them.

Some of these things are less about a compiler than about a development
environment. That's why I brought up literate programming. I look in on the
newsgroup, but noone seems to have picked up on XML, etc.

---
"Alan Grover, Technical Pb" awgrover@umich.edu
+1 (743) 647-5778
Project Leader
Health Media Research Lab, Cancer Center
5D04 North Ingalls Building, Mail Stop 0471
300 North Ingalls
Ann Arbor, MI 48109-0471