writing computer code which corresponds to mathematics
4 views
Skip to first unread message
Joao Marcos
May 3, 2020, 4:27:46 PM5/3/20
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
https://xenaproject.wordpress.com/2020/04/30/the-invisible-map/
"The basic idea: our code will correspond to mathematical definitions
and proofs, and our code will compile if and only if our proofs are
correct. Such systems do exist — but in this post, we will just
imagine what this kind of code might look like, and how easy it would
be for a mathematician to write it. The “de Bruijn factor” of a system
like this is the ratio (size of program which proves a theorem in our
system) / (size of LaTeX file which proves the same theorem), and
ideally this number should be small."
JM
"The basic idea: our code will correspond to mathematical definitions
and proofs, and our code will compile if and only if our proofs are
correct. Such systems do exist — but in this post, we will just
imagine what this kind of code might look like, and how easy it would
be for a mathematician to write it. The “de Bruijn factor” of a system
like this is the ratio (size of program which proves a theorem in our
system) / (size of LaTeX file which proves the same theorem), and
ideally this number should be small."
JM
Reply all
Reply to author
Forward
0 new messages