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.

Note:

• 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.