Learning to use automated proof checkers might be a valuable rationalist-training technique.
Struggling with a compiler or a proof checker (They’re very similar by the Curry-Howard isomorphism) is an interesting (and perhaps depressing) learning experience. The computer reveals how many “details” you can overlook, and how frequently your gut or instinct is just wrong. Often the “details” are the vast majority of the final result.
Some of the appeal that LessWrong has for programmers might be explained by their exposure to this sort of learning experience.
Learning to use automated proof checkers might be a valuable rationalist-training technique.
Struggling with a compiler or a proof checker (They’re very similar by the Curry-Howard isomorphism) is an interesting (and perhaps depressing) learning experience. The computer reveals how many “details” you can overlook, and how frequently your gut or instinct is just wrong. Often the “details” are the vast majority of the final result.
Some of the appeal that LessWrong has for programmers might be explained by their exposure to this sort of learning experience.