Re:Names are not type safety
by bsza on Monday November 02, 2020 @02:35AM
(#24965515)
> It's like saying that a non-machine-checkable mathematical proof is not a proof - something few working mathematicians would agree with.
Only because we're not ready for that yet. Given the current technology (Coq, Agda, Mizar etc.), writing a machine-checkable proof is unbelievably tedious. That doesn't mean it wouldn't be welcome; many published papers, even widely accepted ones, have later been found to contain errors. [1] [2]
Only because we're not ready for that yet. Given the current technology (Coq, Agda, Mizar etc.), writing a machine-checkable proof is unbelievably tedious. That doesn't mean it wouldn't be welcome; many published papers, even widely accepted ones, have later been found to contain errors. [1] [2]
[1] https://mathoverflow.net/questions/35468/widely-accepted-mat...
[2] https://lamport.azurewebsites.net/tla/proof-statistics.html