我有一个 C# 商业应用程序，带有单元测试。我可以通过使用 NModel 或 Spec Explorer 来提高可靠性并减少测试时间和费用吗？或者，如果我用 F#（甚至 Haskell）重写它，我会看到什么样的（如果有的话）可靠性增加？
代码合同？阿斯麦?
我意识到这是主观的，可能是有争议的，所以如果可能的话，请用数据来支持你的答案。:) 或者也许是一个可行的例子，例如 Eric Evans Cargo Shipping System？
如果我们考虑
单元测试是具体的强定理，对特定的“有趣的实例”进行准静态检查，类型是一般但弱的定理（通常静态检查），合同是一般和强定理，动态检查发生在常规程序运行。（来自 B. Pierce 的认为有害的类型），
这些其他工具在哪里适合？
我们可以使用 Java PathFinder、Scala 等为 Java 提出类似的问题。
可靠性是几个变量的函数，包括软件的一般架构、程序员的能力、需求的质量以及配置管理和一般 QA 流程的成熟度。所有这些都会影响重写的可靠性。
话虽如此，语言肯定会产生重大影响。所有其他条件相同：
将所有这些东西放在一起，您应该拥有一个强大的工具包，用于在整个开发生命周期中提高质量。不幸的是，我不知道有任何可靠的研究可以证明这一点。我在开始时列出的所有因素都会混淆任何真正的研究，并且您需要大量数据才能显示出明确的模式。
在我的“第一”语言 C# 的上下文中，对引用的一些评论：
单元测试是具体和强大的定理，
是的，但他们可能不会给你一阶逻辑检查，比如“对于所有 x 都存在 ay，其中 f(y)”，更像是“存在 ay，这里是 (！)，f(y)”，又名设置, 行动, 断言。;)*
对特定的“有趣的实例”进行准静态检查，并且类型是一般但较弱的定理（通常是静态检查），
类型不一定那么弱**。
和合同是一般和强定理，动态检查在常规程序运行期间发生的特定实例。（来自 B. Pierce 的认为有害的类型），
我认为 Pex + Moles 越来越接近一阶逻辑检查类型，因为它会生成边缘情况并使用 C9 求解器来处理整数约束求解。我真的很想看到更多 Moles 教程（moles 用于替换实现），特别是与某种控制容器的反转一起，它可以利用已经存在的抽象类和接口的存根和实际实现。
在C#中，它们相当薄弱，当然：泛型类型/类型允许您为一个操作添加协议语义——即将类型限制在接口上，从某种意义上说，接口是实现类同意的协议。但是，协议的静态类型只针对一种操作。
让我们以 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#，我不知道。
从应用程序的消费端来看，不同的上下文之间可能存在交互，例如调度程序、后台/其他线程，最好我们希望保证我们不会最终陷入死锁。
此外，还需要处理可观察对象的确定性处置。当扩展方法返回的 IObservable 实例处理方法的参数的 IObservable 实例并处理这些实例时，可能一直不清楚，因此需要了解黑盒的内部工作原理（或者您可以放开引用以“合理的方式”，GC会在某个时候接受他们）
实现了 TPL 之上的任务池。在任务池中，我们有一个工作窃取队列，用于在工作线程上调用。
如果我们改变状态，使用 APM/begin/end 或异步模式（排队到任务池）可能会使我们面临回调排序错误。此外，开始调用及其回调的协议可能过于复杂，因此无法遵循。前几天，我阅读了一篇关于 Silverlight 项目的验尸报告，该项目在查看所有回调树的业务逻辑森林时遇到了问题。然后有可能实现穷人的异步 monad，IEnumerable 带有一个异步“管理器”迭代它并在每次产生的 IAsyncResult 完成时调用 MoveNext()。
...不要让我开始研究 IAsyncResult 中的大量隐藏协议。
另一个不使用 Reactive 扩展的问题是海龟问题——一旦你决定你想要一个异步的 IO 阻塞操作，就需要海龟一直到 p/invoke 调用来放置相关的 Win32 线程一个 IO 完成端口！如果您有三层，然后在最顶层内部还有一些逻辑，则需要使所有三层都实现 APM 模式；并履行 IAsyncResult 的众多合同义务（或使其部分损坏）——并且基类库中没有默认的公共 AsyncResult 实现。
即使涵盖了上述内存管理 + 并行性 + 合同 + 协议项，在一个好的、可靠的应用程序中，仍然有例外需要处理（不仅仅是接收和忘记）。我想举个例子；
假设我们发现自己从合约/接口捕获了一个异常（不一定来自反应式扩展的 IObservable 实现，它具有单子异常处理而不是基于堆栈帧）。
希望程序员勤奋并记录可能的异常，但可能一直存在异常可能性。如果一切都用代码契约正确定义，至少我们可以确定我们有能力捕获一些异常，但是许多不同的原因可能集中在一种异常类型中，一旦抛出异常，我们如何确保最小可能尺寸的工作是否得到纠正？
假设我们正在从应用程序中的消息总线消费者推送一些数据记录，并在后台线程上接收它们，该线程决定如何处理它们。
这里的一个现实例子可能是我每天都在使用的 Spotify。
我 100 美元的路由器/接入点会随机放弃。我猜它有一个缓存错误或某种堆栈溢出错误，因为每次我通过它推送超过 2 MB/s 的 LAN/WAN 数据时都会发生这种情况。
我必须启动网卡；wifi和以太网卡。以太网的连接中断。Spotify 事件处理程序循环的套接字返回无效代码（我认为是 C 或 C++）或抛出异常。Spotify 必须处理它，但它不知道我的网络拓扑是什么样的（并且没有代码来尝试所有路由/更新路由表以及要使用的接口）；我仍然有一条通往互联网的路线，但只是不在同一个界面上。Spotify 崩溃。
异常根本不够语义化。我相信可以从 Haskell 中的 Error monad 的角度来看异常。我们要么继续要么中断：展开堆栈、执行捕获、执行 finally，祈祷我们不会在其他异常处理程序或 GC 上出现竞争条件，或者未完成 IO 完成端口的异步异常。
但是当我的一个接口的连接/路由出现故障时，Spotify 崩溃冻结。
现在我们有了 SEH/结构化异常处理，但我认为我们将来会有 SEH2，其中每个异常源都给出了实际异常，一个可区分的联合（即它应该静态类型到链接的库/程序集），可能的补偿动作——在这个例子中，我可以想象 Windows 的网络 API 告诉应用程序执行补偿动作以在另一个接口上打开相同的套接字，或者自己处理它（就像现在一样），或者重试套接字，带有一些内核管理的重试策略。这些选项中的每一个都是可区分联合类型的一部分，因此实现者必须使用其中一个。
我认为，当我们拥有 SEH2 时，它不会再被称为异常。
^^
反正我已经跑题太多了。
与其阅读我的想法，不如听听 Erik Meijer 的一些话——这是他和 Joe Duffy 之间非常好的圆桌讨论。他们讨论处理呼叫的副作用。或者看看这个搜索列表。
今天，作为一名顾问，我发现自己处于维护一个系统的位置，其中更强的静态语义可能是好的，我正在寻找可以给我编程速度+正确性验证水平的工具是准确和精确的。我还没有找到它。
我只是认为我们距离面向开发人员的可靠计算还有 20 年的时间。现在有太多的语言、框架、营销 BS 和概念在空中，普通开发人员无法掌握一切。
因为我发现类型系统将成为解决方案的一部分；类型不必弱！简洁的代码和强类型系统（想想 Haskell）帮助程序员构建可靠的软件。