ニュース

  • 2020.02.28
  • info

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

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

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

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

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

公開日:2020/02/06

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