多分これ?
終わり近くからの抜粋:
別れる前に、プログラミング入門コースでコンピューティングの根本的な目新しさを正義にする次の方法を検討してください。
一方では、述語論理のように見えるものを教えますが、それは哲学者とは非常に異なっています。未解釈の数式の操作について初心者プログラマーをトレーニングするために、論理接続のすべての代数的特性に学生を慣れさせて、ブール代数としてそれをより多く教えます。直感へのリンクをさらに切断するために、ブール領域の値{true、false}の名前を{black、white}に変更します。
一方、基本ステートメントとしてスキップと複数の代入、ローカル変数のブロック構造、ステートメント構成の演算子としてのセミコロン、優れた代替構文、優れた代替構文を使用して、シンプルでクリーンな命令型プログラミング言語を教えます。繰り返し、必要に応じてプロシージャ呼び出し。これに、ブール値、整数、文字、文字列などの最小限のデータ型を追加します。重要なことは、私たちが紹介するものが何であれ、対応するセマンティクスはそれに伴う証明規則によって定義されるということです。
最初から、そしてコース全体を通して、プログラマーの仕事はプログラムを書き留めることだけではなく、彼が提案するプログラムが同様に正式な機能仕様を満たしていることの正式な証明を与えることであることを強調します。証明とプログラムを連携して設計している間、学生は述語計算で彼の操作の敏捷性を完成させる十分な機会を得ます。最後に、この入門プログラミングコースは主に形式数学のコースであるというメッセージを伝えるために、問題のプログラミング言語がキャンパスに実装されていないため、学生がプログラムをテストする誘惑から保護されていることがわかります。 。これで、新入生向けのプログラミング入門コースの提案のスケッチは終わりです。