crash.academyの新着講座公開のお知らせ：2月

crash.academy(ITエンジニア向け学習＆キャリアサービス)に、今月新たに公開された講座をご紹介します。

■IT技術とCoqの世界 – 「証明」＝「プログラム」＝「計算」の意味を考える


■ 動画紹介
Coqは、一般には「証明支援システム」と呼ばれています。多くのIT技術者にとって、Coqは、特殊な分野（数学の問題の証明等）での特殊なコンピュータの利用だという印象を与えるかもしれません。
ただ、Coqにできることと、IT技術者が日常的に行っていることとの間には、実は、大きな共通点があります。

あらためて確認したいのは、IT技術者にとって一番身近な対象であるプログラムが、極めて「論理的」な性格を持つということです。プログラミングするときに、我々は営業トークやプレゼンをする時とは違った頭を使います。
それは端的に言って、「論理的」に考えるということだと思います。プログラムの「意図」を、プログラマは論理的にコードとして実装します。

公開日：2020/02/06

冒頭部分は無料でご視聴いただけます。
ぜひご覧ください。