4 ms·

Very fundamental ideas around computability, or total vs partial functions. There are some correctness properties that we can prove without running the underlyi

by Silfen 9y ago

Very fundamental ideas around computability, or total vs partial functions. There are some correctness properties that we can prove without running the underlying program, such that we can always accept or reject a given program. None of this is particular to lisp.

shalabhc 9y ago
Fundamental ideas about computability include the model of the Turing machine, which has no notion of types, verification, or even functions whatsoever - there are just too many degrees of freedom. I agree there are correctness properties we can prove without running a 'program', but how do we map the notion of a 'program' into the real world. Is a single function a program? A single module which includes multiple functions? A single executable? A single system that includes multiple processes communicating over a network? I'm arguing each of these is a 'program' and a Turing machine in the theoretical sense. Each of these programs is hooked up to other 'programs' outside of it. 'Compilation' requires the input to be static, but if we think about how things are in flux (you can change a function, switch out a shared library or upgrade and restart a running process, etc.) when do you verify that a 'program' is 'correct'? This is what I mean by 'compile time is made-up' - it falls out of the current frame of thinking of one OS process = one program = static set of source files. It is possible to design systems that have no notion of 'compile time'. You could still have verification, but it could be incremental and spread out all through the lifetime of the running system. So the system would have no 'compile phase' - it would be running live and as you update parts of it, the updated parts would integrate with the rest of the system and do verification like things.

4 ms·

Very fundamental ideas around computability, or total vs partial functions. There are some correctness properties that we can prove without running the underlyi

by Silfen 9y ago

shalabhc 9y ago
Fundamental ideas about computability include the model of the Turing machine, which has no notion of types, verification, or even functions whatsoever - there are just too many degrees of freedom. I agree there are correctness properties we can prove without running a 'program', but how do we map the notion of a 'program' into the real world. Is a single function a program? A single module which includes multiple functions? A single executable? A single system that includes multiple processes communicating over a network? I'm arguing each of these is a 'program' and a Turing machine in the theoretical sense. Each of these programs is hooked up to other 'programs' outside of it. 'Compilation' requires the input to be static, but if we think about how things are in flux (you can change a function, switch out a shared library or upgrade and restart a running process, etc.) when do you verify that a 'program' is 'correct'? This is what I mean by 'compile time is made-up' - it falls out of the current frame of thinking of one OS process = one program = static set of source files. It is possible to design systems that have no notion of 'compile time'. You could still have verification, but it could be incremental and spread out all through the lifetime of the running system. So the system would have no 'compile phase' - it would be running live and as you update parts of it, the updated parts would integrate with the rest of the system and do verification like things.