Poly/ML

In spite of the fact that the original ML and its immediate descendants were never really widely used, they had an enormous influence over other programming languages that took some of the innovations it had to bring. Then again, if you are still using or maybe just tackling its potential, then there is a good chance that you are looking for a compiler.

Poly/ML is an advanced implementation of Standard ML and the preferred choice for large theorem prover projects, including HOL4 and Isabelle. The highlight of the tool stems from the fact that it is capable of checking the code as you write and even provides suggestions as to why the particular line is problematic, such as forgetting to declare the value, for instance.

The tool packs a source-level debugger and hence, you can use it to set the breakpoints in the program and point the values of local variables, depending on your project. Take note that the debugger can be accessed via the command line by default, but it can be integrated into the existing IDE structures.

The utility can call functions that are written in other programming languages and allows both static and dynamic libraries. However, you should bear in mind that these commands need to be in a format which the C-function can understand.