3 ms·

Never ever. Humans are idiots. If you build machines like humans you will get idiotic machines. Machines need to do things exactly right and not almost right or

by ceving 3y ago

Never ever. Humans are idiots. If you build machines like humans you will get idiotic machines. Machines need to do things exactly right and not almost right or mostly right. Current AI trends will not create better machines, just more idiotic machines. Those idiotic machines will be sufficient to impress idiots, but they will not help to do things exactly right. Automated theorem proving is the only way to build better machines.

ta8645 3y ago
> Automated theorem proving is the only way to build better machines. Sure, but that will just be one aspect of an integrated and wholistic AI, which can configure the parameters input to the automated theorem proving component, and act on the results.
samatman 3y ago
Automated theorem proving will only ever be an arrow in the quiver, because even in theory, the space of useful computer programs is a vast superset of those which may have all their properties formally verified. In practice, it's a much larger superset than theory allows. Growing the space of formally verifiable subprograms is a worthy endeavor, sure, but so is good old-fashioned engineering.
funcDropShadow 3y ago
> Automated theorem proving is the only way to build better machines. That is only true for a very narrow notion of "better machines". Automated theorem proving is still light years away from being applicable in the majority of software projects. Don't get me wrong I am aware of the progress made in the last decades. Yet, it will be some time until someone writing the next iOS app will reach routinely for an automated theorem prover to lower the defect rate. And even then, the questions remains whether fulfilling a formal specification is at all correlated with "better machines" or "better software". There are domains where this is conceivable: os kernels (L4), certifying compilers (CompCert), and others. But how does a theorem prover, automated or not, help with improving the next generations of video codecs? That is an intrinsically subjective problem -- the quality axis, less so the performance axis. How does theorem proving help with neuronal networks? How does it help with capturing the right business process to actually improve business outcomes and not just introducing new bureaucracy?

by ceving 3y ago

ta8645 3y ago

> Automated theorem proving is the only way to build better machines. Sure, but that will just be one aspect of an integrated and wholistic AI, which can configure the parameters input to the automated theorem proving component, and act on the results.

samatman 3y ago

Automated theorem proving will only ever be an arrow in the quiver, because even in theory, the space of useful computer programs is a vast superset of those which may have all their properties formally verified. In practice, it's a much larger superset than theory allows. Growing the space of formally verifiable subprograms is a worthy endeavor, sure, but so is good old-fashioned engineering.

funcDropShadow 3y ago

> Automated theorem proving is the only way to build better machines. That is only true for a very narrow notion of "better machines". Automated theorem proving is still light years away from being applicable in the majority of software projects. Don't get me wrong I am aware of the progress made in the last decades. Yet, it will be some time until someone writing the next iOS app will reach routinely for an automated theorem prover to lower the defect rate. And even then, the questions remains whether fulfilling a formal specification is at all correlated with "better machines" or "better software". There are domains where this is conceivable: os kernels (L4), certifying compilers (CompCert), and others. But how does a theorem prover, automated or not, help with improving the next generations of video codecs? That is an intrinsically subjective problem -- the quality axis, less so the performance axis. How does theorem proving help with neuronal networks? How does it help with capturing the right business process to actually improve business outcomes and not just introducing new bureaucracy?