What does HackerNews think of tis-interpreter?

What makes you think they don't understand it? They acknowledge that it is UB. I read them as realistic, since they know that people rely on C compilers working a certain way. They even wrote an interpreter that detects UB: https://github.com/TrustInSoft/tis-interpreter

I understand why people like the compiler being able to leverage UB. I suspect this philosophy actually makes Trust-In-Soft more money: You could argue that if there was no UB, there would be no need for the tis-interpreter.

So isn't it in fact quite self-less that they encourage the world to optimize a bit less (spending more money on 'compute'), while standing to profit from the unintended behaviour they'd otherwise be contracted to help debug?

It's true, but there's a few tools out there to help now, such as tis-interpreter (https://github.com/TrustInSoft/tis-interpreter)

There are some tools aimed roughly in this direction, such as https://github.com/TrustInSoft/tis-interpreter.

A major difficulty here is that undefined behaviour is a property of a particular execution of a C program, rather than a static property of the program itself. Tools that dynamically detect UB are useful, but will not demonstrate that there are no inputs for which a program will go wrong.

Have you tried using tis-interpreter [0] (an interpreter of C for detecting undefined behavior written in OCaml) written by Pascal Cuoq [1].

[0] https://github.com/TrustInSoft/tis-interpreter

[1] http://stackoverflow.com/users/139746/pascal-cuoq

Thanks for that. Looks like only SPARK is available in the operating system that I use. That is one big problem with research software and software research, it is often disconnected from the programmer community.

BTW, what do you think of this tool?

https://github.com/TrustInSoft/tis-interpreter