3 ms·

I get your point, and I agree with it too. My comment is (trying to) say that in those cases we don't know that humans are any better! Your other comment has s

I get your point, and I agree with it too. My comment is (trying to) say that in those cases we don't know that humans are any better! Your other comment has some problems, but a better example is fn collatz(mut n: bigint, mut v: Vec<...>) { loop { n = { if n%2==0 then n/2 else 3\*n+1 }; v.push(...); } } As far as we know, we can't bound the memory usage of this program: and if any FM can do it as well then there's a million bucks on the table. But so far no human can do it either! And if your program relies on this program using bounded memory, from an engineering perspective you're kind of SOL no matter what. On the other hand, if you're writing programs which humans are pretty sure they know why the properties they want hold (as we usually try to do, anyways), then translating this into a machine-checked proof can give you a lot more faith that the property actually holds and possibly even find flaws in your reasoning/implementation if there are any!

kaba0 3y ago
Yes I agree with you on every point (though didn’t want to use the “heavy gunner” Collatz as an example :D). I’m not against dependent types, and I eagerly await what future might they bring. But at the same time I think the best solution will be to “fight on multiple fronts”, and improve our type and test systems. There are very interesting ways to systematically test every kind of input (greatly reducing the input space) that has a distinct code path (and it can find a minimal reproducible error case!).
reuben364 3y ago
Well one thing programmers do often due to the complexity of formal proof is random property testing instead. Mathematicians do so too, which is why the Collatz conjecture is a conjecture in the first place. There is an alternative to Software Foundations that uses randomized property checking. It would be interesting to have a hybrid system where we independently give specifications and then decide whether we wanted to formally prove them or just do tests instead.

kaba0 3y ago

Yes I agree with you on every point (though didn’t want to use the “heavy gunner” Collatz as an example :D). I’m not against dependent types, and I eagerly await what future might they bring. But at the same time I think the best solution will be to “fight on multiple fronts”, and improve our type and test systems. There are very interesting ways to systematically test every kind of input (greatly reducing the input space) that has a distinct code path (and it can find a minimal reproducible error case!).

reuben364 3y ago

Well one thing programmers do often due to the complexity of formal proof is random property testing instead. Mathematicians do so too, which is why the Collatz conjecture is a conjecture in the first place. There is an alternative to Software Foundations that uses randomized property checking. It would be interesting to have a hybrid system where we independently give specifications and then decide whether we wanted to formally prove them or just do tests instead.