私の「最初の」言語であるC＃のコンテキストでの引用に関するいくつかのコメント：
単体テストは具体的で強力な定理であり、
はい。ただし、「すべての x について、f(y) の場合に y が存在する」、「y が存在する、ここでは (!)、f(y) である」、別名 setup などの最初の順序のロジック チェックが提供されない場合があります。 、行動する、主張する。;)*
特定の「興味深いインスタンス」について準静的にチェックし、タイプは一般的ですが弱い定理です（通常は静的にチェックされます）。
型は必ずしもそれほど弱いわけではありません**。
契約は一般的で強力な定理であり、通常のプログラム操作中に発生する特定のインスタンスを動的にチェックします。(B. ピアースの「有害と見なされるタイプ」から)、
単体テスト
Pex + Moles は、エッジ ケースを生成し、C9 ソルバーを使用して整数制約の解決を行うため、一次論理型のチェックに近づいていると思います。Moles のチュートリアル (moles は実装を置き換えるためのものです) をもっと見たいと思っています。具体的には、抽象クラスとインターフェイスのスタブ実装と実際の実装が既に存在するものを活用できる、ある種のコントロール コンテナーの反転と一緒です。
弱いタイプ
C#では、それらは確かにかなり弱いです。一般的な型付け/型を使用すると、 1 つの操作にプロトコルのセマンティクスを追加できます。つまり、型をインターフェース上に制限することができます。これは、ある意味では実装クラスが同意するプロトコルです。ただし、プロトコルの静的型付けは1 回の操作のみです。
例: リアクティブ拡張 API
Reactive Extensions を議論のトピックとして取り上げましょう。
オブザーバブルによって実装された、消費者が必要とするコントラクト。
interface IObserver<in T> : IDisposable {
void OnNext(T);
void OnCompleted();
void OnError(System.Exception);
}
プロトコルには、このインターフェイスが示す以上のものがあります。IObserver< in T > インスタンスで呼び出されるメソッドは、次のプロトコルに従う必要があります。
注文:
OnNext{0,n} (OnCompleted | OnError){0, 1}
さらに、別の軸で。時間次元:
時間：
for all t|-> t:(method -> time). t(OnNext) < t(OnCompleted)
for all t|-> t:(method -> time). t(OnNext) < t(OnError)
つまり、OnCompleted xor OnError への呼び出しの後に OnNext への呼び出しを行うことはできません。
さらに、平行度の軸:
並列性:
no invocation to OnNext may be done in parallel
つまり、IObservable の実装者が従わなければならないスケジューリングの制約があります。IObservable は、最初にコンテキストの呼び出しを同期せずに、複数のスレッドから同時にプッシュすることはできません。
このコントラクトの保持を簡単な方法でテストするにはどうすればよいですか? C#では、わかりません。
API の利用者
アプリケーションの消費側からすると、 Dispatcher、バックグラウンド/その他のスレッドなど、異なるコンテキスト間で相互作用が発生する可能性があり、できればデッドロックに陥らないことを保証したいと考えています。
さらに、オブザーバブルの決定論的な破棄を処理する必要があります。拡張メソッドの返された IObservable インスタンスがメソッドの引数の IObservable インスタンスを処理し、それらを破棄する時期が常に明確であるとは限らないため、ブラック ボックスの内部動作について知る必要があります (または、参照を手放すことができます)。 「合理的な方法」で、GC はある時点でそれらを取得します)
<<< Reactive Extensions がなければ、必ずしも簡単ではありません。
TPLの上にタスクプールが実装されています。タスク プールには、ワーカー スレッドで呼び出すデリゲートのワーク スティーリング キューがあります。
APM/begin/end または async パターン (タスク プールのキューに入れる) を使用すると、状態を変更すると、コールバック順序のバグが発生する可能性があります。また、begin-invocations とそのコールバックのプロトコルが複雑すぎるため、従うことができない場合があります。先日、すべてのコールバック ツリーのビジネス ロジック フォレストを表示する際に問題が発生した Silverlight プロジェクトについての事後調査を読みました。次に、貧しい人の非同期モナドを実装する可能性があります。IEnumerable を非同期の「マネージャー」で反復処理し、生成された IAsyncResult が完了するたびに MoveNext() を呼び出します。
...そして、IAsyncResult 内の無数の隠しプロトコルについて、私を始めさせないでください。
Reactive 拡張機能を使用しない場合のもう 1 つの問題は、タートルの問題です。IO ブロッキング操作を非同期にすることを決定したら、関連する Win32 スレッドを配置する p/invoke 呼び出しまでずっとタートルが必要です。 IO完了ポート！3 つのレイヤーがあり、最上位レイヤー内にいくつかのロジックがある場合、3 つのレイヤーすべてに APM パターンを実装させる必要があります。IAsyncResult の多数のコントラクトの義務を果たします (または部分的に壊れたままにします)。基本クラス ライブラリには、デフォルトの public AsyncResult 実装はありません。
>>>
インターフェイスからの例外の処理
上記のメモリ管理 + 並列処理 + コントラクト + プロトコルの項目がカバーされていても、優れた信頼性の高いアプリケーションでは、(受け取って忘れるだけでなく)処理する必要のある例外がまだあります。例を挙げたいと思います。
環境
コントラクト/インターフェイスから例外をキャッチしていることに気付いたとしましょう (必ずしもスタック フレーム ベースではなくモナド例外処理を行うリアクティブ拡張の IObservable 実装からではありません)。
プログラマーが勤勉で、考えられる例外を文書化していれば幸いですが、例外の可能性はずっとあるかもしれません。すべてがコード コントラクトで正しく定義されている場合、少なくともいくつかの例外をキャッチできると確信できますが、多くの異なる原因が 1 つの例外タイプ内にまとめられている可能性があります。最小サイズの作品が修正されていることを確認しますか?
標的
アプリケーションのメッセージ バス コンシューマーからデータ レコードをプッシュし、バックグラウンド スレッドでそれらを受け取り、処理を決定するとします。
例
ここでの実際の例は、私が毎日使用している Spotify です。
私の 100 ドルのルーター/アクセス ポイントは、ランダムなタイミングでタオルを投入します。2 MB/秒を超える LAN/WAN データをプッシュするたびに発生するため、キャッシュ バグまたは何らかのスタック オーバーフロー バグがあると思います。
NIC をアップする必要があります。wifiとイーサネットカード。イーサネットの接続がダウンします。Spotify のイベント ハンドラ ループのソケットは、無効なコード (C または C++ だと思います) を返すか、例外をスローします。Spotify はそれを処理する必要がありますが、私のネットワーク トポロジがどのように見えるかはわかりません (そして、すべてのルートを試したり、ルーティング テーブルを更新したり、使用するインターフェイスを更新したりするコードはありません)。インターネットへのルートはまだありますが、同じインターフェイス上ではありません。Spotify がクラッシュします。
論文
例外は単にセマンティックではありません。Haskell の Error モナドの観点から例外を見ることができると思います。続行するか中断します。スタックを巻き戻し、キャッチを実行し、finally を実行して、他の例外ハンドラーまたは GC で競合状態に陥ったり、未処理の IO 完了ポートの非同期例外が発生したりしないことを祈ります。
しかし、インターフェイスの接続/ルートの 1 つがダウンすると、Spotify がクラッシュしてフリーズします。
現在、SEH/構造化例外処理がありますが、将来的には SEH2 になると思います。ここでは、各例外ソースが実際の例外とともに識別共用体 (つまり、リンクされたライブラリ/アセンブリに静的に型付けする必要があります) を提供します。この例では、Windows のネットワーク API がアプリケーションに補正アクションを実行して別のインターフェイスで同じソケットを開くか、それを独自に処理するか (今のように)、再試行するように指示することを想像できます。カーネル管理の再試行ポリシーを使用します。これらの各オプションは、判別共用体型の一部であるため、実装者はそれらのいずれかを使用する必要があります。
SEH2になったら、もう例外と呼ばれなくなると思います。
^^
とにかく、私はすでに脱線しすぎています。
私の考えを読む代わりに、Erik Meijer のいくつかを聞いてください。これは、彼と Joe Duffy の間の非常に優れた円卓会議です。彼らは、呼び出しの副作用の処理について議論しています。または、この検索リストをご覧ください。
私は今日、コンサルタントとして、より強力な静的セマンティクスが有効なシステムを維持する立場にいることに気付きました。正確で正確です。私はまだそれを見つけていません。
開発者指向の信頼できるコンピューティングから遠く離れていない場合でも、あと 20 年はかかると思います。現在、あまりにも多くの言語、フレームワーク、マーケティング BS、および概念が飛び交っているため、通常の開発者が物事を把握することはできません。
これが「弱いタイプ」の見出しの下にあるのはなぜですか?
型システムが解決策の一部になることがわかったからです。タイプは弱い必要はありません！簡潔なコードと強力な型システム (Haskell を考えてください) は、プログラマーが信頼性の高いソフトウェアを構築するのに役立ちます。