"I have a mind like a steel... uh... thingy." Patrick Logan's weblog.

Search This Blog

Sunday, May 04, 2003

Dynamic Model Checking

Lambda the Ultimate has this piece on a Scheme program that analyzes Excel spreadsheets.

What is most notable about this? The essence of this system represents the future of software development and the need for more dynamic analysis than "compilers" traditionally give.


  • Scheme is a dynamic language.
  • The program analyzes spreadsheets.
  • Spreadsheets are another dynamic language.

This represents the convergence of dynamic model checking and infered static type checking. The future is getting more dynamic and so "type checkers" will become more sophisticated (and background) theorem provers than they are now.

Additional features will include symbolic execution including concurrency model checking and semi-symbolic partial evaluation.

Over the last 10-15 years electronics design has taken more of a software design flavor. Over the next 10-15 years software design will take on more of a traditional hardware simulation and model checking flavor.

No comments:

Blog Archive

About Me

Portland, Oregon, United States
I'm usually writing from my favorite location on the planet, the pacific northwest of the u.s. I write for myself only and unless otherwise specified my posts here should not be taken as representing an official position of my employer. Contact me at my gee mail account, username patrickdlogan.