4 ms·

Indeed proof formalisms are themselves leaky abstractions.

• cannabis_sam 6y ago
  The theories, the implementations, or both?
  • mbrock 6y ago
    The theories as conceived to relate to the actual programming environment. Any proof about a Haskell program’s correctness relies on a leaky abstraction (an axiomatization) of what will actually happen when you run GHC on the source file.
    • cannabis_sam 6y ago
      So implementation then..
      • mbrock 6y ago
        The theory is supposed to be an abstraction of the implementation, not the other way around...
        • cannabis_sam 6y ago
          Supposed by whom?