Is it possible to prove anything about IO calls?

Stream: new members

[Dan Abramov]

This isn't anything practical but I'm curious if it's possible to prove anything about a program like this.

def main := do
  IO.println "Hello"

Or is it fully opaque to theorems?

[Eric Wieser]

Well, you can prove main = main, or something like

def main := do
  IO.println "Hello"

def main2 := do
  IO.println ("H" ++ "ello")

example : main = main2 := rfl

[Eric Wieser]

But IO.println ultimately calls docs#IO.getStdout, which is opaque

[Alfredo Moreira-Rosa]

or even :

theorem exist_string_printed_main :
  ∃ (s : String), main = IO.println s := by
  use "Hello"
  rfl

[Alfredo Moreira-Rosa]

so definitely not opaque

[Dan Abramov]

I see, so I guess I can't unfold getStdout (which makes sense) but I can in principle unfold other stuff (including main itself and even some intermediate functions before we get too deep, though maybe that breaks encapsulation too much).