3 ms·
Perhaps that could be a new 'job' in itself? "Proof programmer": persons specialized in formalizing proof statements. So if you're an experienced PP maybe the s
by darkmighty 11y ago
Perhaps that could be a new 'job' in itself? "Proof programmer": persons specialized in formalizing proof statements. So if you're an experienced PP maybe the statement above becomes easy. Or you use a proof in a 'library' of sorts that let's you proof that. If
1) Proofs are well defined enough in the first place that you don't need great insight to understand them;
2) The time of some mathematicians is very invaluable;
3) Formalizing/verifying statements is sufficiently useful for mathematicians;
then they might be useful?
- ende 11y agoI can see the headline now... "Show HN: Pudding - A language for programming proofs". I could see a lot of uses for this kind of programming. In a language like Matlab or R, we just assume that the implementations correctly match the theoretical methods they implement, but anyone who has deleved into the internals of some published R library knows that's not always the case. With the expanded use of pure functional languages for more closely mapping method to implementation, proof programming could offer a useful form of unit testing to the development of libraries.