3 ms·
A good path to this might be deeper investigation of logic/constraint programming. Its a good tool for formally encoding known, discrete constraints like you de
by dgb23 6y ago
A good path to this might be deeper investigation of logic/constraint programming. Its a good tool for formally encoding known, discrete constraints like you described above.
- infogulch 6y agoAgreed! I've been paying attention to constraint/logic programming (CLP) recently, but I haven't found the right thing yet / haven't invested enough time into it to find the right thing. In my very-layman opinion, CLP-based systems need three things to properly take off: 1. some kind of 'type system'-like thing that enables robust symbolic reasoning over pure relations in any mode, 2. a critical mass of defined layers that is 'deep enough' to reach the hardware, 3. a way to express verified alternatives and preference in the order they are applied.
- infogulch 6y agoIMO an interesting project in this space is: mm0 / MetaMath Zero - Closing the loop in proof verification down to verifying the machine code of the verifier. Goes from first-order logic to peano arithmetic to a model of x86 to a model of the verifier written in x86. Interestingly, it demonstrates that verification of a compact proof can be performed in linear time (!) if the proof is structured correctly. -- https://github.com/digama0/mm0 https://github.com/digama0/mm0 The fact that proof checking can take linear time (though not proof-finding), and the fact that it incorporates so many 'layers' has emboldened my opinion that such a thing as I described above is possible and has enormous potential.