How can the `log` function be used for formal verification

Question

In JavaScript I want to create a log function:

function log(string) {
  console.log(string)
}

Obviously this causes side effects; it prints to the screen. And I have no control over its implementation. Basically, I just trust that it works.

But I wonder what I can do to incorporate something like this into a formal verification system. Maybe I make it into some sort of Monad, but I have a hard time understanding how Monads work. It seems that I want to say something about an abstract global state which goes from one state to another, as in

log(string) = state -> state'

But I'm not really sure what I can do from there, or what this even gives me. I would like to say something about how this function is verified, but I'm not sure what that would take, if it is just tests of some degree, or if I can write a specification that doesn't require understanding the complete implementation.

Please let me know what I can do with this situation, how I can take this log function and integrate it into an otherwise pure verification system.

Answer 1

Formal verification needs to have a goal: what precisely do you want to prove?

For example, if you merely want to prove that a program terminates than you can treat built-in functions like console.log() as a given and declare an axiom that the function terminates. You can then use that axiom to prove whether user-defined functions that call console.log() also terminate.

If you want to prove more complicated properties such as multiple outputs are written in a specific order, then using things like an IO monad could be helpful. The monad properties themselves are not useful here, simply because JavaScript has no such built-in concept. Instead, it would be useful to model every function as taking a “state of the world” token as an implicit parameter. Each token can be used exactly once; and I/O functions consume a token and produce an new token. You can then use data flow analysis, SSA, or something like C++'s or Rust's ownership system to track these tokens and consequently the ordering of operations.

For many other kinds of formal verification, for example when trying to address the question whether a function returns the correct result, you can simply ignore console.log() as it returns no value.

So: first determine your goals, then find an appropriate formal verification framework, then (if necessary) find a way to model this function within your formal semantics.