Loading [MathJax]/jax/output/CommonHTML/config.js

开发者社区

文档建议反馈控制台

文章/答案/技术大牛

发布

社区首页 >问答首页 >标准ML的稳健性证明？

问标准ML的稳健性证明？
EN

Stack Overflow用户

提问于 2013-12-06 15:15:02

回答 2查看 266关注 0票数 5

关于标准ML编译器，我的问题是，尽管ML本身是正式定义的，可以证明程序的确定性计算，但编译器本身不是用C编写的吗?C不是正式定义的，至少不是全部？我想我的问题是，假设我们用标准ML编写了一个程序，可以证明它的正确性，我们怎么知道C编写的编译器没有以一种可能改变结果的方式执行呢？

谢谢

compiler-construction

大模型视频创作引擎特惠

提供高质量视频生成与处理服务，技术领先、效果专业、应用广泛，新用户3折起！

EN

回答 2

Stack Overflow用户

回答已采纳

发布于 2013-12-06 15:23:02

这是一个责任问题。不管您的SML运行时或编译器是用哪种语言编写的(SML是一种规范，而SML编译器做的是而不是，它可以是任何其他语言)，您的责任是使您的SML程序按照SML规范工作。如果SML编译器是错误的，那是其他人的问题。

您是否考虑过处理器、SML运行时的编译指令？谁正式证明了这一点？那么在处理器的晶体管中移动的电子呢？谁告诉他们按照处理器设计所依据的物理“定律”工作？谁正式证明了这些法律？

这不是你的问题。

这就是说，在撰写本文时，有一个用Coq，CompCert编写的C编译器。这个编译器为输入语言(大部分C语言)和目标汇编语言定义了形式语义。只要SML实现设计为在编译时使用这种风格的C，则输入语言不必完全是C。如果您使用CompCert的输入语言实现了SML，并且尽可能地遵循正式定义，那么您将拥有一个SML解释器，它的信任链几乎不间断地下降到程序集。

票数 3

EN

Stack Overflow用户

发布于 2013-12-06 15:24:03

仅仅因为你可以写坏的C程序并不意味着你必须写。完全有可能编写正确的C程序，并从C语言规范中推断程序执行正确。

票数 3

EN

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/20435282

复制

相关文章

TLS协议分析 (三) record协议

SSL 证书 https http 网络安全数据加密服务

record协议做应用数据的对称加密传输，占据一个TLS连接的绝大多数流量，因此，先看看record协议图片来自网络:

用户8964349

2021/09/06

1.4K0

TLS握手协议详解

https SSL 证书

握手协议是TLS握手协议的一部分，负载生成共享密钥以及交换证书。其中，生成共享密钥是为了进行密码通信，交换证书是为了通信双方相互进行认证。

用户9407507

2022/02/16

1.3K0

TLS协议学习笔记

安全 https 编程算法 nat

说起TLS(Transport Layer Security 传输层安全协议)，可能有点陌生，但是说起HTTPS，大家应该都知道，我们现在浏览网页基本上都是HTTPS的。HTTPS就是加密的HTTP，HTTP基于明文传播，直接使用HTTP的话内容很容易被窃取。HTTPS则对内容进行了一层加密，避免了内容被窃取和篡改的可能性，如下图所示。

roper

2018/07/02

2.4K1

mqttnet 详解_mqttnet3.0用法

mqtt javascript node.js https 网络安全

1 ///开源库地址：https://github.com/chkr1011/MQTTnet

全栈程序员站长

2022/09/12

1K0

图解TLS握手连接

文件存储 SSL 证书 https

SSL：（Secure Socket Layer，安全套接字层），位于可靠的面向连接的网络层协议和应用层协议之间的一种协议层。SSL通过互相认证、使用数字签名确保完整性、使用加密确保私密性，以实现客户端和服务器之间的安全通讯。该协议由两层组成：SSL记录协议和SSL握手协议。

半月弧

2020/03/03

5.4K0

TLS协议分析 (四) handshake协议概览

数据加密服务 SSL 证书 es 编程算法文件存储

TLS 1.3对握手做了大修改，下面先讲TLS 1.2，讲完再介绍一下分析TLS 1.3.

用户8964349

2021/09/07

1.5K0

TLS协议分析 (六) handshake协议扩展

SSL 证书数据加密服务 https 网络安全

在 ChangeCipherSpec 消息之后，应该立即发送 Finished 消息，来确认密钥交换和认证过程已经成功了。ChangeCipherSpec 必须在其它握手消息和 Finished 消息之间。

用户8964349

2021/09/07

1.3K0

DTLS协议介绍，Udp协议基于TLS

网络安全 SSL 证书全站加速网络缓存专用宿主机

UDP协议是不面向连接的不可靠协议，且没有对传输的报文段进行加密，不能保证通信双方的身份认证、消息传输过程中的按序接收、不丢失和加密传送。

Kunkka Wu

2022/01/13

3.1K0

DTLS协议介绍，Udp协议基于TLS

mqttnet 详解_mqttnet 简记

mqtt https 网络安全 javascript node.js

1.mqttnet开源库，https://github.com/chkr1011/MQTTnet

全栈程序员站长

2022/09/12

3K0

MQTTnet[通俗易懂]

mqtt java https 网络安全

近期学习了一下物联网中应用较广的MQTT协议，同时使用MQTTnet开源类库做了简单实现，因此做下笔记。环境：.NET Framework 4.6.1 MQTTnet 2.8.2.0 遵循MQTT 3.1.0协议规范源码 >>> GitHub 注意：在实现订阅者离线再连接时，一直接受不到离线信息，需要做一下配置

全栈程序员站长

2022/09/12

7970

mqttnet 详解_MQTT MQTTnet 实现

mqtt javascript 编程算法 https java

│ │ ├── MQTTServer.runtimeconfig.dev.json

全栈程序员站长

2022/09/12

9210

检查网站的TLS版本

网站安全 rsa sha tls

有时候需要知道某个网站支持的TLS的版本。现在SSL 2.0和SSL 3.0都已经被淘汰了。其中TLS 1.0，TLS 1.1，TLS 1.2是目前的的主流，相对也是安全的。主要看加密的算法。TLS 1.3是目前最新的协议版本，也是相对最安全的版本了。

宋天伦

2023/10/21

4.4K0

轻量通讯协议 --- MQTT

mqtt 测试客户端连接协议

「MQTT（Message Queuing Telemetry Transport）」是一种轻量级的消息传输协议，通常用于在物联网（IoT）和传感器网络中进行通信。它设计用于在低带宽、不稳定或高延迟的网络环境下传输数据，因此非常适用于连接设备之间的通信，尤其是在资源有限的环境中。

Niuery Diary

2023/10/22

4.1K0

轻量通讯协议 --- MQTT

TLS加密远程连接Docker

SSL 证书 tcp/ip 容器镜像服务 https linux

版权声明：本文为博主原创文章，遵循 CC 4.0 BY-SA 版权协议，转载请附上原文出处链接和本声明。

程序员欣宸

2019/09/18

2.1K0

TLS加密远程连接Docker

如何建立TLS连接？TLS握手失败可能这个原因！

tls 加密客户端连接算法

签前面三个案例里的HTTP都没加密，使排查工作省去不少麻烦，抓包文件里直接就看清应用层信息。

JavaEdge

2023/07/25

1.4K0

如何建立TLS连接？TLS握手失败可能这个原因！

mqttnet 详解_MQTTnet 3.0.5学习笔记

c++mqtt java 编程算法 android

段时间在使用MQTTnet，都说这个东西比较好,可是翻了翻网上没有例子给参考一下。

全栈程序员站长

2022/09/12

1.1K0

golang简单tls协议用法完整示例

本文实例讲述了golang简单tls协议用法。分享给大家供大家参考，具体如下：生成私钥： openssl genrsa -out key.pem 2048 生成证书： openssl req -new -x509 -key key.pem -out cert.pem -days 3650 https： package main import ( "io" "net/http" "log" ) func HelloServer(w http.ResponseWrite

李海彬

2018/03/27

3.8K0

golang简单tls协议用法完整示例

本文实例讲述了golang简单tls协议用法。分享给大家供大家参考，具体如下：生成私钥： openssl genrsa -out key.pem 2048 生成证书： openssl req -new -x509 -key key.pem -out cert.pem -days 3650 https： package main import ( "io" "net/http" "log" ) func HelloServer(w http.ResponseWriter, req *

李海彬

2018/03/26

3.3K0

SSL / TLS 协议运行机制详解

本文简要介绍SSL/TLS协议的运行机制。文章的重点是设计思想和运行过程，不涉及具体的实现细节。如果想了解这方面的内容，请参阅RFC文档。

Java技术栈

2018/07/30

8130

SSL / TLS 协议运行机制详解

点击加载更多

相似问题

AttributeError：“函数”对象没有属性“as_view”

18

Django "AttributeError：‘函数’对象没有属性'as_view'“

11

AttributeError - CBV‘函数’对象没有属性'as_view‘。

12

AttributeError:输入对象'DirectView‘没有属性'as_view’

10

AttributeError：'function‘对象没有属性'as_view’。怎么了？

22

活动推荐

体验智能媒资降冷，云点播优惠不要错过！

添加站长进交流群

领取专属 10元无门槛券

AI混元助手 在线答疑

关注 腾讯云开发者公众号

洞察 腾讯核心技术

剖析业界实践案例