crash.academy(ITエンジニア向け学習&キャリアサービス)に、今月新たに公開された講座をご紹介します。
■IT技術とCoqの世界 – 「証明」=「プログラム」=「計算」の意味を考える
■ 動画紹介
Coqは、一般には「証明支援システム」と呼ばれています。多くのIT技術者にとって、Coqは、特殊な分野(数学の問題の証明等)での特殊なコンピュータの利用だという印象を与えるかもしれません。
ただ、Coqにできることと、IT技術者が日常的に行っていることとの間には、実は、大きな共通点があります。
あらためて確認したいのは、IT技術者にとって一番身近な対象であるプログラムが、極めて「論理的」な性格を持つということです。プログラミングするときに、我々は営業トークやプレゼンをする時とは違った頭を使います。
それは端的に言って、「論理的」に考えるということだと思います。プログラムの「意図」を、プログラマは論理的にコードとして実装します。
公開日:2020/02/06
冒頭部分は無料でご視聴いただけます。
ぜひご覧ください。
Contact usお問い合わせ
サービスにご興味をお持ちの方は
お気軽にお問い合わせください。
Webからお問い合わせ
お問い合わせお電話からお問い合わせ
03-5211-7750
平日09:30 〜 18:00
Free Service