4 ms·
It uses formal methods to verify that the generated machine code has the same behavior as the source program.
by steinuil 9y ago
It uses formal methods to verify that the generated machine code has the same behavior as the source program.
- tytytytytytytyt 9y agoThat's not at all helpful - I meant specific examples...
- chrisseaton 9y agoThey mean 'correct' in the technical PL sense. So they don't mean there are specific things that are incorrect in MLton - there may not be any examples anyone can give you - they mean that we don't know mathematically how correct MLton is or not, because nobody has done that work, and we do know to a better extent mathematically that CakeML is correct, because it has been mathematically proven to be correct to a certain degree.