3 ms·
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 axi
by 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 agoSo implementation then..
- mbrock 6y agoThe theory is supposed to be an abstraction of the implementation, not the other way around...
- cannabis_sam 6y agoSupposed by whom?