- 型と値は区別する必要がある。
- 計算と演算を区別するのは難しい。曖昧に区別されていることもあるが、混同して使っても差し支えない。
- 関数と計算は一応区別するが、ヘッド部（後述）の有る無しの違いしかないので、混同して使っても差し支えない。
- 型と型の非空性宣言（後述）は区別する必要がある。
- 関数の存在宣言（後述）と関数の実装要求（後述）は区別する必要がある。
- プログラミングとメタプログラミング（プログラムをデータとみなして操作するプログラミング）は区別する必要がある。
|- null string, number |- boolean string, number |-? boolean
| 型 | 命題 |
| 型の値 | 命題の証拠 |
| 計算 | 証明 |
| 関数 | 定理 |
| 演算 | 推論 |
| 存在宣言 | 証明可能性判断 |
| 非空宣言 | 命題の証明可能性判断 |
| プログラミング | 証明作業 |
| メタプログラミング | リーズニング作業 |
| 関数定義のヘッド部 | 定理記述のヘッド部 |
- 証明作業とリーズニング作業は区別する必要がある。
- 証明と推論を区別するのは難しい。曖昧に区別されていることもあるが、混同して使っても差し支えない。
- 定理と証明は一応区別するが、ヘッド部（後述）の有る無しの違いしかないので、混同して使っても差し支えない。
- 命題と証拠は区別する必要がある。
- 命題と命題の証明可能性判断は区別する必要がある。
- 定理の証明可能性判断と定理の証明要求は区別する必要がある。
現状：
- 証明作業とリーズニング作業を区別してない、またはゴッチャにしている場合が多い。
- 証明と推論を区別していて、その区別を絶対視している場合がある。
- 定理と証明を区別していて、まったく違うものとして扱っていることがある。
- 命題と証拠を区別してない、またはゴッチャにしている場合が多い。
- 命題と命題の証明可能性判断を区別してない、またはゴッチャにしている場合が多い。
- 定理の証明可能性判断と定理の証明要求を区別してない、またはゴッチャにしている場合が多い。
| 関数定義 | 定理記述 |
| 関数定義のヘッド部 | 定理記述のヘッド部 |
| 関数定義のボディ部 | 定理記述の証明部 |
| 関数定義のプロファイル部 | 定理記述のステートメント部 |
| プロファイルの引数の型 | ステートメントの前提の命題 |
| プロファイルの戻り型 | ステートメントの結論の命題 |
