{"id":2953,"date":"2020-10-14T18:51:56","date_gmt":"2020-10-14T10:51:56","guid":{"rendered":"https:\/\/sosconf.org\/?p=2953"},"modified":"2020-10-27T14:54:25","modified_gmt":"2020-10-27T06:54:25","slug":"sosconf-zh-speaker-series-interviews-7","status":"publish","type":"post","link":"https:\/\/sosconf.org\/zh-hans\/sosconf-zh-speaker-series-interviews-7\/","title":{"rendered":"2020\u4e2d\u6587\u5b66\u751f\u5f00\u6e90\u5e74\u4f1a\u538b\u8f74\u8bb2\u8005\u4e13\u8bbf\uff1aICE1000\/\u5343\u91cc\u51b0\u5c01"},"content":{"rendered":"<p>2020\u4e2d\u6587\u5b66\u751f\u5f00\u6e90\u5e74\u4f1a\u5c06\u4e8e10\u670818\u65e5\u4e0a\u5348\u4e5d\u70b9\u4e8e<a href=\"https:\/\/live.bilibili.com\/22566724\" rel=\"nofollow noopener\" target=\"_blank\"><strong>bilibili 22566724\u76f4\u64ad\u95f4<\/strong><\/a>\u5f00\u542f\u76f4\u64ad\uff0c\u5728\u672c\u6b21\u6d3b\u52a8\u4e4b\u524d\uff0c\u5f00\u6e90\u5e74\u4f1a\u7ec4\u59d4\u4f1a\u7279\u522b\u63a8\u51fa\u8bb2\u8005\u7cfb\u5217\u4e13\u8bbf\uff1a\u4ece\u5373\u65e5\u8d77\u81f310\u670818\u65e5\uff0c\u6211\u4eec\u5c06\u4e3a\u6bcf\u4f4d\u8bb2\u8005\u63a8\u51fa\u4e00\u7bc7\u72ec\u5bb6\u4e13\u8bbf\u3002<\/p>\n<p>\u672c\u6b21\u4e13\u8bbf\u4e3a\u6b64\u6b212020\u4e2d\u6587\u5b66\u751f\u5f00\u6e90\u5e74\u4f1a\u7cfb\u5217\u4e13\u8bbf\u552f\u4e00\u7684\u7ebf\u4e0b\u4e13\u8bbf\uff0c\u53d7\u8bbf\u8005\u5343\u91cc\u51b0\u5c01\/ICE1000\uff08\u4ee5\u4e0b\u4ee5\u201c\u51b0\u51b0\u201d\u7b80\u79f0\uff09\u4e0d\u4ec5\u5e26\u6765\u4e86\u8fd9\u671f\u8d28\u91cf\u6781\u9ad8\u7684\u8bbf\u8c08\uff0c\u540c\u65f6\u4e5f\u4f5c\u4e3a\u4e00\u4f4d\u201c\u6210\u90fd\u571f\u8457\u201d\uff0c\u5e26\u9886\u7b14\u8005\u6e38\u89c8\u4e86\u8bb8\u591a\u6210\u90fd\u5e02\u4e2d\u5fc3\u9c9c\u4e3a\u4eba\u77e5\u7684\u597d\u53bb\u5904\u3002<\/p>\n<p>\u4e0e\u51b0\u51b0\u89c1\u9762\u662f\u5728\u901a\u60e0\u95e8\u5730\u94c1\u7ad9\uff0c\u7b14\u8005\u7684\u7b2c\u4e00\u611f\u89c9\u662f\uff1a\u5927\u4f6c\u7684\u5934\u50cf\u786e\u5b9e\u662f\u7d20\u989c\u51fa\u955c\uff08\u7b11\uff09\u3002<\/p>\n<p>\u51b0\u51b0\u5e26\u9886\u7b14\u8005\u53bb\u4e86\u4e00\u5bb6\u5192\u83dc\u9986\u5b50\u3002\u4ed6\u900f\u9732\uff0c\u8fd9\u9986\u5b50\u7684\u8001\u677f\u4e0e\u4ed6\u662f\u8001\u719f\u4eba\uff0c\u8001\u677f\u66fe\u89c1\u8bc1\u8fc7\u51b0\u51b0\u89c1\u8fc7\u7684\u56db\u4f4d\u7f51\u53cb\uff0c\u7b14\u8005\u662f\u8001\u677f\u6240\u89c1\u8bc1\u7684\u7b2c\u4e94\u4f4d\u3002\u8fd9\u4e2a\u9986\u5b50\u7684\u5473\u9053\u4e5f\u7684\u786e\u4e0a\u4e58\uff0c\u51b0\u51b0\u4ecb\u7ecd\u7684\u51e0\u79cd\u5192\u83dc\u6599\u5341\u5206\u7f8e\u5473\uff0c\u4e3a\u7b14\u8005\u5f00\u542f\u4e86\u65b0\u4e16\u754c\u3002<\/p>\n<p>\u996d\u540e\uff0c\u6211\u4eec\u7a7f\u8fc7\u5bbd\u7a84\u5df7\u5b50\u3001\u7a7f\u8fc7\u4eba\u6c11\u516c\u56ed\u3001\u7a7f\u8fc7\u660f\u9ec4\u7684\u706f\u5149\uff0c\u6765\u5230\u6ce1\u6850\u6811\u8857\uff0c\u6210\u90fd\u4e0d\u4e3a\u4eba\u77e5\u7684\u4e00\u9762\u5c55\u73b0\u5728\u7b14\u8005\u7684\u773c\u524d\u3002\u6211\u4eec\u5728\u4e00\u5bb6\u9152\u5427\u5f00\u59cb\u4e86\u91c7\u8bbf\uff0c\u5e2d\u95f4\uff0c\u51b0\u51b0\u6388\u6743\u6211\u4eec\u4e3a\u4ed6\u62cd\u4e0b\u4e86\u51e0\u5f20\u7167\u7247\uff0c\u7559\u4f5c\u7eaa\u5ff5\u3002<img loading=\"lazy\" decoding=\"async\" class=\"aligncenter wp-image-2958 size-full\" src=\"https:\/\/sosconf.org\/wp-content\/uploads\/2020\/10\/DSC07327-2-scaled.jpg\" alt=\"\" width=\"2560\" height=\"1708\" srcset=\"https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/DSC07327-2-scaled.jpg 2560w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/DSC07327-2-300x200.jpg 300w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/DSC07327-2-1024x683.jpg 1024w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/DSC07327-2-768x512.jpg 768w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/DSC07327-2-1536x1025.jpg 1536w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/DSC07327-2-2048x1366.jpg 2048w\" sizes=\"auto, (max-width: 2560px) 100vw, 2560px\" \/><\/p>\n<p>\u4e13\u8bbf\uff0c\u6b63\u5f0f\u5f00\u59cb\u3002<\/p>\n<p><strong>Q1:\u00a0<\/strong><strong>\u611f\u8c22\u60a8\u80fd\u62bd\u7a7a\u63a5\u53d7\u6211\u4eec\u7684\u91c7\u8bbf\uff0c\u8bf7\u95ee\u60a8\u80fd\u5148\u505a\u4e00\u4e2a\u81ea\u6211\u4ecb\u7ecd\u5417\uff1f<\/strong><\/p>\n<p><strong>ICE1000<\/strong><strong>\uff1a<\/strong>OK\uff0c\u6211\u662f\u6700\u8001\u7684\u90a3\u4e00\u5c4a00\u540e\uff0c\u662f\u4e2a\u6c34\u8d27\uff0c\u5199\u8fc7\u4e00\u4e9b\u5fae\u4e0d\u8db3\u9053\u7684\u4ee3\u7801\uff0c\u505a\u8fc7\u4e00\u4e9b\u5fae\u5c0f\u7684\u8d21\u732e\u3002\u5728\u6280\u672f\u65b9\u9762\uff0c\u6211\u5bf9\u590d\u6742\u7f16\u7a0b\u8bed\u8a00\u7684\u7c7b\u578b\u7cfb\u7edf\u7684\u5b9e\u73b0\u548c\u8bbe\u8ba1\u4ee5\u53ca\u5404\u79cd\u7f16\u7a0b\u5de5\u5177\u94fe\uff0c\u5305\u62ecIDE\u7684\u5f00\u53d1\u975e\u5e38\u611f\u5174\u8da3\u3002<\/p>\n<p><strong>Q2<\/strong><strong>:\u8bf7\u95ee<\/strong><strong>\u201c\u5343\u91cc\u51b0\u5c01\/ICE1000\u201d\u8fd9\u4e2aID\u662f\u4ece\u4f55\u800c\u6765\u5462\uff1f<\/strong><\/p>\n<p><strong>ICE1000<\/strong>\uff1a\u201c\u5343\u91cc\u51b0\u5c01\u201d\u8fd9\u4e2a\u540d\u5b57\u7684\u6765\u6e90\u662f\u5f88\u65e9\u5f88\u65e9\u7684\u4e8b\u60c5\uff0c\u662f\u5c0f\u5b66\u7684\u65f6\u5019\u770b\u5230\u8d5b\u5c14\u53f7\u7684\u4e00\u4e2a\u670d\u52a1\u5668\u7684\u540d\u5b57\u53eb\u5343\u91cc\u51b0\u5c01\uff0c\u6211\u4e2a\u4eba\u5f88\u559c\u6b22\u8fd9\u4e2a\u540d\u5b57\uff0c\u4e8e\u662f\u5c31\u628a\u5b83\u53d8\u6210\u4e86\u6211\u7684\u5168\u7f51ID\uff1b\u4f46\u5728\u67d0\u4e9b\u53ea\u652f\u6301\u82f1\u6587\u5b57\u7b26\u7684\u7f51\u7ad9\u4e0a\u8fd9\u4e2aID\u662f\u4e0d\u53ef\u7528\u7684\uff0c\u4e8e\u662f\u6211\u5c31\u60f3\u6574\u4e00\u4e2a\u7ffb\u8bd1\uff1b\u4f46\u8fd9\u4e2a\u8bcd\u7ec4\u65e0\u8bba\u600e\u4e48\u7ffb\u8bd1\u90fd\u662f\u4e00\u4e2a\u975e\u5e38\u957f\u7684\u8bcd\u7ec4\uff0c\u8fd9\u4e0d\u5229\u4e8e\u6211\u529f\u6210\u540d\u5c31\u4e4b\u540e\u8ba9\u522b\u4eba\u8bb0\u4f4f\u6211\u7684\u540d\u5b57\uff0cICE1000\u5c31\u662f\u8fd9\u4e48\u88ab\u7ffb\u8bd1\u51fa\u6765\u5e76\u4f7f\u7528\u81f3\u4eca\u7684\u3002\u540e\u6765\u6211\u7ed9\u81ea\u5df1\u8d77\u4e86\u4e2a\u66f4\u50cf\u4eba\u540d\u7684\u7f51\u540d\uff0cTesla Ice Zhang\u3002\u539f\u56e0\u662f\u6211\u975e\u5e38\u559c\u6b22Nikola Tesla\u8fd9\u4f4d\u79d1\u5b66\u5bb6\uff0c\u540c\u65f6\u4e5f\u6709\u5f88\u591a\u4eba\u559c\u6b22\u53eb\u6211ICE\uff0c\u51b0\u51b0\u7b49\u7b49\uff0c\u8fd9\u4e2a\u8eab\u4efd\u548c\u6211\u7684\u4e09\u6b21\u5143\u8eab\u4efd\u5f3a\u76f8\u5173\u4e86\uff0cICE\u4fbf\u6210\u4e3a\u4e86\u8fd9\u4e2aID\u7684\u4e2d\u95f4\u540d\u4e86\u3002<strong><img loading=\"lazy\" decoding=\"async\" class=\"aligncenter wp-image-2961 size-full\" src=\"https:\/\/sosconf.org\/wp-content\/uploads\/2020\/10\/michael-dziedzic-VlZYu3nZIRI-unsplash-scaled.jpg\" alt=\"\" width=\"2560\" height=\"1925\" srcset=\"https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-VlZYu3nZIRI-unsplash-scaled.jpg 2560w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-VlZYu3nZIRI-unsplash-300x226.jpg 300w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-VlZYu3nZIRI-unsplash-1024x770.jpg 1024w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-VlZYu3nZIRI-unsplash-768x578.jpg 768w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-VlZYu3nZIRI-unsplash-1536x1155.jpg 1536w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-VlZYu3nZIRI-unsplash-2048x1540.jpg 2048w\" sizes=\"auto, (max-width: 2560px) 100vw, 2560px\" \/><\/strong><\/p>\n<p><strong>Q3: \u8bf7\u95ee\u80fd\u5411\u6211\u4eec\u7b80\u8981\u5730\u4ecb\u7ecd\u4e00\u4e0b\u60a8\u7684\u6f14\u8bb2\u7684\u5185\u5bb9\u5417\uff1f<\/strong><\/p>\n<p><strong>ICE1000\uff1a<\/strong>\u200b\u6211\u7684\u7814\u7a76\u65b9\u5411\u662f\u7f16\u7a0b\u8bed\u8a00\uff0c\u5176\u4e2d\u6211\u6bd4\u8f83\u611f\u5174\u8da3\u7684\u65b9\u5411\u662f\u590d\u6742\u7684\u7c7b\u578b\u7cfb\u7edf\uff0c\u4f46\u8fd9\u6b21\u6211\u53ef\u80fd\u4e0d\u4f1a\u53bb\u8bb2\u590d\u6742\u7684\u7c7b\u578b\u7cfb\u7edf\uff0c\u56e0\u4e3a\u8fd9\u6837\u9762\u5411\u7684\u7fa4\u4f53\u5b9e\u5728\u592a\u5c0f\u4e86\uff1b\u800c\u7b80\u5355\u7684\u7c7b\u578b\u7cfb\u7edf\u4e5f\u6709\u8bb8\u591a\u53ef\u8bb2\u4e4b\u5904\uff0c\u5c24\u5176\u662fJava\u7cfb\u8bed\u8a00\u7684\u7c7b\u578b\u7cfb\u7edf\u4e0eHaskell\u7cfb\u8bed\u8a00\u7684\u7c7b\u578b\u7cfb\u7edf\uff0c\u8fd9\u4e24\u8005\u662f\u6709\u7740\u6bd4\u8f83\u7ed3\u6784\u5316\u7684\u533a\u522b\u7684\u3002\u8fd9\u4e9b\u4e1c\u897f\u53ef\u4ee5\u8f85\u52a9\u4f60\u4ece\u4e00\u4e2a\u66f4meta(\u5143)\u7684\u89d2\u5ea6\u770b\u5f85\u7f16\u7a0b\u8bed\u8a00\u4e0e\u7f16\u7a0b\u8fd9\u4ef6\u4e8b\u672c\u8eab\u3002\u53e6\u5916\u4e00\u4e2a\u65b9\u5411\u5c31\u662f\u8bbe\u8ba1\u6a21\u5f0f\uff0c\u4f46\u8fd9\u4e2a\u4e1c\u897f\u88ab\u8bef\u89e3\u7684\u5f88\u5389\u5bb3\uff0c\u6240\u4ee5\u8fd9\u6b21\u6211\u60f3\u4ece\u6211\u81ea\u5df1\u7684\u89d2\u5ea6\u8bb2\u8bb2\u3002\u6211\u4e00\u76f4\u62b1\u6709\u8fd9\u6837\u7684\u4e00\u4e2a\u89c2\u5ff5\uff1a\u6bcf\u4e00\u79cd\u8bbe\u8ba1\u6a21\u5f0f\u90fd\u6709\u4e00\u4e2a\u76f8\u5bf9\u5e94\u7684\u8bed\u8a00\u7279\u6027\u3002\u4f8b\u5982Java\u8fd9\u79cd\u8bed\u8a00\u7279\u6027\u5f88\u5c11\u7684\u8bed\u8a00\uff0c\u5b83\u7684\u8bbe\u8ba1\u6a21\u5f0f\u5c31\u4f1a\u76f8\u5bf9\u6bd4\u8f83\u591a\uff1b\u800c\u7279\u6027\u6bd4\u8f83\u591a\u7684\u8bed\u8a00\u5219\u4f1a\u628a\u4e00\u4e9b\u8bbe\u8ba1\u6a21\u5f0f\u505a\u6210\u8bed\u8a00\u7279\u6027\u3002\u7f16\u7a0b\u8bed\u8a00\u8981\u4e48\u505a\u5f97\u5f88\u7b80\u5355\uff0c\u5c06\u7f16\u5199\u8bbe\u8ba1\u6a21\u5f0f\u7684\u6743\u9650\u7559\u7ed9\u7528\u6237\uff1b\u8981\u4e48\u505a\u5f97\u5f88\u590d\u6742\uff0c\u5c06\u8bbe\u8ba1\u6a21\u5f0f\u505a\u6210\u8bed\u8a00\u7279\u6027\u3002\u4f46\u65e0\u8bba\u600e\u6837\uff0c\u8bbe\u8ba1\u8005\u65e0\u6cd5\u963b\u6b62\u7528\u6237\u6765\u624b\u5199\u8bbe\u8ba1\u6a21\u5f0f\uff0c\u5f53\u8bed\u8a00\u7279\u6027\u4e0d\u6ee1\u8db3\u7528\u6237\u7684\u9700\u6c42\u7684\u65f6\u5019\uff0c\u7528\u6237\u53c8\u4f1a\u56de\u5230\u4e4b\u524d\u539f\u59cb\u7684\u65b9\u5f0f\u53bb\u624b\u5199\u8bbe\u8ba1\u6a21\u5f0f\u3002<\/p>\n<p><strong>Q4:\u00a0<\/strong><strong>\u76ee\u524d\u6709\u76f8\u5f53\u4e00\u90e8\u5206\u4eba\u8ba4\u4e3a\u7528\u4e0a\u8bbe\u8ba1\u6a21\u5f0f\u4e4b\u540e\u4ee3\u7801\u4f1a\u53d8\u5f97\u590d\u6742\u4e0e\u5197\u4f59\uff0c\u4f46\u662f\u4e5f\u6709\u539f\u6559\u65e8\u4e3b\u4e49\u8005\u89c9\u5f97\u4ec0\u4e48\u90fd\u5e94\u8be5\u7528\u8bbe\u8ba1\u6a21\u5f0f\uff0c\u8bf7\u95ee\u60a8\u5982\u4f55\u770b\u5f85\u8fd9\u4e2a\u95ee\u9898\u7684\u5462\uff1f<\/strong><\/p>\n<p><strong>ICE1000\uff1a<\/strong>\u5bf9\u4e8e\u524d\u4e00\u79cd\u89c2\u70b9\uff0c\u6211\u4e2a\u4eba\u611f\u89c9\u4e0d\u662f\u8fd9\u4e48\u4e00\u56de\u4e8b\u3002\u9996\u5148\uff0cIDE\u53ef\u4ee5\u5e2e\u52a9\u7528\u6237\u5efa\u7acb\u8bbe\u8ba1\u6a21\u5f0f\u7684\u6a21\u578b\uff0c\u5c06\u6240\u6709\u6210\u5458\u53d8\u91cf\u90fd\u5efa\u7acb\u597d\uff1b\u4f46\u662f\u4e5f\u4f1a\u6709\u4eba\u8ba4\u4e3a\u81ea\u52a8\u5199\u8d77\u6765\u65b9\u4fbf\uff0c\u8bfb\u8d77\u6765\u5374\u5f88\u9ebb\u70e6\u3002\u5728\u6211\u770b\u6765\uff0c\u8bbe\u8ba1\u6a21\u5f0f\u7684\u4ee3\u7801\u5176\u5b9e\u90fd\u662f\u4e00\u4e2a\u6a21\u5b50\u91cc\u523b\u51fa\u6765\u7684\uff0c\u4e00\u4e2a\u51e0\u767e\u884c\u7684\u6587\u4ef6\uff0c\u6709\u7684\u65f6\u5019\u8bfb\u5230\u524d\u4e09\u884c\u4f60\u5c31\u80fd\u77e5\u9053\u4ee3\u7801\u7684\u5168\u8c8c\u3002\u8fd9\u610f\u5473\u7740\u5982\u679c\u4f5c\u8005\u4e25\u683c\u9075\u5faa\u8bbe\u8ba1\u6a21\u5f0f\uff0c\u4e0d\u4ec5\u80fd\u591f\u63d0\u5347\u4ee3\u7801\u7684\u53ef\u8bfb\u6027\uff0c\u8fd8\u80fd\u591f\u964d\u4f4e\u6574\u4e2a\u4ee3\u7801\u7684\u7ef4\u62a4\u6210\u672c\u3002\u5bf9\u4e8e\u540e\u4e00\u79cd\u89c2\u70b9\uff0c\u6211\u4eec\u53ef\u4ee5\u7ad9\u5728\u7c7b\u578b\u7cfb\u7edf\u7684\u89d2\u5ea6\u6765\u89e3\u91ca\u3002\u8fd9\u4e2a\u95ee\u9898\u80fd\u591f\u901a\u8fc7\u4e0d\u540c\u7684\u7c7b\u578b\u7cfb\u7edf\u6765\u89e3\u51b3\uff1a\u4e0d\u540c\u7684\u7c7b\u578b\u7cfb\u7edf\u4e0b\u4f1a\u62e5\u6709\u4e0d\u540c\u7684\u8bbe\u8ba1\u6a21\u5f0f\uff0c\u5728\u6211\u770b\u6765\u8bbe\u8ba1\u6a21\u5f0f\u5c31\u662f\u5c31\u662f\u4f60\u60f3\u5b8c\u6210\u4e00\u4ef6\u4e8b\uff0c\u7136\u540e\u628a\u4ee3\u7801\u5199\u6210\u4e00\u4e2a\u7279\u5b9a\u7684\u683c\u5f0f\uff0c\u8fd9\u662f\u4e00\u4e2a\u611f\u6027\u7684\u5b9a\u4e49\u3002\u6bd4\u5982\u8bf4\u5f02\u5e38\u5728\u4e00\u822c\u8bed\u8a00\u4e2d\u662f\u8bed\u8a00\u7279\u6027\uff0c\u4f46\u662f\u5728Haskell\u548cRust\u4e2d\u6ca1\u6709\u8fd9\u4e2a\u8bed\u8a00\u7279\u6027\uff0c\u5b83\u4eec\u90fd\u662f\u7528\u5e93\u5b8c\u6210\u7684\u3002\u8bbe\u8ba1\u6a21\u5f0f\u6211\u4e2a\u4eba\u611f\u89c9\u90fd\u53ef\u4ee5\u662f\u5728\u5b66\u7f16\u7a0b\u65f6\u81ea\u5df1\u53d1\u73b0\u7684\uff0c\u56e0\u4e3a\u6709\u7684\u8bbe\u8ba1\u6a21\u5f0f\u5b9e\u5728\u662f\u592a\u7b80\u5355\u4e86\uff0c\u4ee5\u81f3\u4e8eHaskell\u793e\u533a\u8bb8\u591a\u65f6\u5019\u90fd\u4e0d\u628a\u8fd9\u4e9b\u4e1c\u897f\u53eb\u505a\u8bbe\u8ba1\u6a21\u5f0f\uff0c\u800c\u662f\u5355\u72ec\u4f7f\u7528\u540d\u5b57\u6765\u79f0\u547c\u4ed6\u4eec\uff0c\u6bd4\u5982 Profunctor Lens, Tagless Final, MTL, Extensible Effects\u8fd8\u6709 Agda \u90a3\u8fb9\u7684totally free\u7b49\u3002\u6709\u4e00\u4e9b\u590d\u6742\u7684\u8bbe\u8ba1\u6a21\u5f0f\u53ef\u80fd\u96be\u4ee5\u81ea\u884c\u53d1\u660e\uff0c\u8fd9\u65f6\u5019\u53ef\u80fd\u624d\u5c31\u9700\u8981\u53bb\u5b66\u4e60\u8fd9\u4e9b\u524d\u4eba\u603b\u7ed3\u7684\u8bbe\u8ba1\u6a21\u5f0f\u3002<\/p>\n<p><strong>Q5: \u8bf7\u95ee\u60a8\u7814\u7a76\u7c7b\u578b\u7cfb\u7edf\u7684\u7684\u5951\u673a\u662f\u4ec0\u4e48\u5462\uff1f<\/strong><\/p>\n<p><strong>ICE1000\uff1a<\/strong>\u672c\u6765\u53ea\u662f\u60f3\u7814\u7a76\u7c7b\u578b\u7cfb\u7edf\u80fd\u591f\u5f3a\u5927\u5230\u4ec0\u4e48\u7a0b\u5ea6\uff0c\u7136\u540e\u53d1\u73b0\u524d\u6cbf\u7684\u7c7b\u578b\u7cfb\u7edf\u786e\u5b9e\u725b\u903c\uff0c\u201c\u4f46\u662f\u7c7b\u578b\u7cfb\u7edf\u5b83\u725b\u903c\u5230\u4e00\u5b9a\u7a0b\u5ea6\u4e4b\u540e\u5c31\u6ca1\u5565\u5b9e\u9645\u7528\u9014\u4e86\u201d\u540e\u6765\u6211\u4e86\u89e3\u5230\u7c7b\u578b\u7cfb\u7edf\u7684\u5e94\u7528\u573a\u666f\u662f\u6709\u9650\u7684\uff0c\u6240\u4ee5\u6211\u5c31\u653e\u5f03\u4e86\u201c\u6709\u7528\u201d\uff0c\u53bb\u7814\u7a76\u6ca1\u7528\u4f46\u662f\u597d\u73a9\u7684\u7c7b\u578b\u7cfb\u7edf\u4e86\uff0c\u5c24\u5176\u662f\u90a3\u4e9b\u5bf9\u63a8\u5bfc\u4e0d\u53cb\u597d\uff0c\u4f46\u662f\u672c\u8eab\u66f4\u5f3a\u5927\u7684\u7c7b\u578b\u7cfb\u7edf\uff0c\u4e5f\u5c31\u662fdependent type\u3002\u7136\u540e\u6211\u4e86\u89e3\u5230\u8fd9\u4e2a\u7406\u8bba\u4e5f\u53ef\u4ee5\u7528\u4e8e\u505a\u5f62\u5f0f\u5316\u9a8c\u8bc1\uff0c\u4e8e\u662f\u6211\u5c31\u5929\u5929\u5728\u7f51\u4e0a\u5439\u5f62\u5f0f\u5316\u9a8c\u8bc1\u597d\u725b\u903c\uff0c\u56e0\u4e3a\u8fd9\u662f\u6700\u590d\u6742\u7684\u7c7b\u578b\u7cfb\u7edf\u7684\u5b9e\u9645\u5e94\u7528\u3002\u7136\u800c\u540e\u6765\u6211\u7ecf\u5386\u4e86\u4e00\u4e9b\u4e8b\u60c5\uff0c\u53d1\u73b0\u5f62\u5f0f\u5316\u9a8c\u8bc1\u5176\u5b9e\u5e76\u4e0d\u9002\u5408dependent type\u53bb\u89e3\u51b3\uff0c\u8fd9\u662f\u53e6\u5916\u4e00\u4e2a\u8bdd\u9898\u4e86\u30022019\u5e74\u6211\u5728\u77e5\u4e4e\u4e0a\u53d1\u4e86\u4e00\u7bc7\u6587\u7ae0\uff0c\u53eb\u300a\u770b\u4e2a\u5934\u300b\uff08look ahead\uff09\uff0c\u5c31\u662f\u5c55\u671b\u672a\u6765\u7684\u610f\u601d\u3002\u5176\u4e2d\u5927\u6982\u8868\u8ff0\u4e86\u4e00\u4e0b\u6211\u7684\u5fc3\u6001\u8f6c\u53d8\uff1a\u5f62\u5f0f\u5316\u9a8c\u8bc1\u4e0d\u5e94\u8be5\u7528dependent type\u7c7b\u578b\u7cfb\u7edf\uff0c\u800c\u662f\u5e94\u8be5\u7528\u53e6\u5916\u4e00\u79cd\u53eb\u505a\u81ea\u52a8\u8bc1\u660e\u7684\u624b\u6bb5\u3002\u5f62\u5f0f\u5316\u9a8c\u8bc1\u5e94\u8be5\u7528\u4e00\u79cd\u5bf9\u4e8e\u9a8c\u8bc1\u66f4\u53cb\u597d\u7684\u65b9\u6cd5\uff0c\u800c\u4e0d\u662f\u7528 Dependent type\u8fd9\u79cd\u66f4\u52a0\u5f62\u5f0f\u5316\u7684\u65b9\u6cd5\uff1b\u6211\u8ba4\u4e3aRefinement Type\u975e\u5e38\u5f62\u5f0f\u5316\uff0c\u5b83\u662f decidedly correct\uff08\u7edd\u5bf9\u6b63\u786e\uff09\u7684\u3002\u9996\u5148\u5b83\u5177\u6709decidable\uff08\u53ef\u5224\u5b9a\u6027\uff09\uff0c\u53ef\u4ee5\u5728\u591a\u5143\u7d20\u590d\u6742\u5ea6\u5185\u89e3\u51b3\u95ee\u9898\uff0c\u81f3\u5c11\u81ea\u52a8\u8bc1\u660e\u7684type checking\uff08\u7c7b\u578b\u68c0\u67e5\uff09\u662fdecidable\u7684\u3002\u540c\u65f6\u5b83\u4e5f\u662fcorrect\u7684\uff0c\u610f\u601d\u662f\u884c\u4e3a\u662f\u786e\u5b9a\u7684\u3002\u786e\u5b9a\u7684\u610f\u601d\u662f\u5176\u7684\u7b97\u6cd5\u4e0e\u884c\u4e3a\u662f\u53ef\u4ee5\u88ab\u51c6\u786e\u63cf\u8ff0\u7684\uff0c\u4e0d\u50cf\u673a\u5668\u5b66\u4e60\u4e0e\u81ea\u52a8\u8bc1\u660e\u6709\u7740\u5404\u79cd\u795e\u79d8\u4f18\u5316\uff1b\u4f46dependent type\u4e0d\u4e00\u6837\uff0c\u4ed6\u662fdecidable\u4e0ecorrect\u7684\uff0c\u6211\u4e2a\u4eba\u4e0d\u559c\u6b22undecidable not correct\u7684\u4e1c\u897f\u3002\u800c\u7c7b\u578b\u7cfb\u7edf\u7684\u8fd9\u79cddependent type\u5c31\u662f\u6211\u559c\u6b22\u7684decidable correct\u7684\uff0c\u6211\u4e2a\u4eba\u611f\u89c9\u5b83\u5f88\u5e72\u51c0\uff1a\u5b83\u7684type checking\u80fd\u591f\u5728\u591a\u9879\u5f0f\u590d\u6742\u5ea6\u5185\u786e\u5b9a\u4ee3\u7801\u662ftype correct\uff08\u7c7b\u578b\u6b63\u786e\uff09\uff0c\u8fd8\u662ftype error\uff08\u7c7b\u578b\u9519\u8bef\uff09\u7684\u3002\u8ba9\u5b83\u6765\u505a\u6570\u5b66\u5b9a\u7406\u7684\u9a8c\u8bc1\u7684\u4ee5\u53ca\u6570\u5b66\u7684\u5f62\u5f0f\u5316\u6211\u611f\u89c9\u518d\u5408\u9002\u4e0d\u8fc7\u4e86\u3002<img loading=\"lazy\" decoding=\"async\" class=\"alignnone wp-image-2959 size-full\" src=\"https:\/\/sosconf.org\/wp-content\/uploads\/2020\/10\/michael-dziedzic-gEN5Btvf2Eg-unsplash-scaled.jpg\" alt=\"\" width=\"2560\" height=\"2011\" srcset=\"https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-gEN5Btvf2Eg-unsplash-scaled.jpg 2560w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-gEN5Btvf2Eg-unsplash-300x236.jpg 300w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-gEN5Btvf2Eg-unsplash-1024x804.jpg 1024w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-gEN5Btvf2Eg-unsplash-768x603.jpg 768w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-gEN5Btvf2Eg-unsplash-1536x1207.jpg 1536w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-gEN5Btvf2Eg-unsplash-2048x1609.jpg 2048w\" sizes=\"auto, (max-width: 2560px) 100vw, 2560px\" \/>\u8fd9\u5f88\u6709\u610f\u4e49\uff0c\u9996\u5148\u662f\u56e0\u4e3a\u5b83\u80fd\u89e3\u51b3\u6570\u5b66\u884c\u4e1a\u7684\u4e00\u4e9b\u95ee\u9898\uff1a\u6570\u5b66\u4e2d\u7684\u4e00\u822c\u7684\u8bc1\u660e\u90fd\u662f\u7528\u81ea\u7136\u8bed\u8a00\u63cf\u8ff0\u7684\uff0c\u800c\u5982\u679c\u4f7f\u7528\u7c7b\u578b\u7cfb\u7edf\u53bb\u63cf\u8ff0\uff0c\u5176\u5c06\u4f1a\u4f7f\u7528\u8bed\u6cd5\u6811\uff0c\u7531\u673a\u5668\u53ef\u4ee5\u9a8c\u8bc1\uff0c\u5f53\u6211\u4eec\u8bf4\u670d\u4e86\u673a\u5668\uff0c\u8bc1\u660e\u4f60\u8fdb\u884c\u9a8c\u8bc1\u8fc7\u7a0b\u5bf9\u4e86\uff0c\u5176\u4ed6\u4eba\u5c31\u53ea\u9700\u8981\u770b\u7ed3\u8bba\u5c31\u597d\u4e86\uff0c\u56e0\u4e3a\u5b83\u662f\u53ef\u4ee5\u65e0\u6570\u6b21\u88ab\u673a\u5668\u6240\u590d\u73b0\u7684\uff0c\u800c\u4e14\u8fd8\u6709\u4e00\u70b9\u4ee3\u7801\u662f\u53ef\u4ee5\u8fdb\u884c\u4e00\u4e9b\u53d8\u6362\u7684\uff0c\u8b6c\u5982\u5728\u673a\u5668\u8bc1\u660e\u4e2d\uff0clemma\uff08\u5f15\u7406\uff09\u662f\u4e00\u4e2a\u51fd\u6570\uff0c\u4f20\u8f93\u4e00\u4e9b\u6761\u4ef6\u7ed9\u51fd\u6570\uff0c\u5b83\u5c31\u80fd\u8fd4\u56de\u4e00\u4e2a\u5b9a\u7406\u3002\u51fd\u6570\u662f\u6709\u51fd\u6570\u4f53\u7684\uff0c\u51fd\u6570\u4f53\u662f\u4e00\u4e2a\u5f88\u5927\u7684\u8868\u8fbe\u5f0f\uff0c\u90a3\u4e48\uff0c\u5f53\u6211\u5199\u4e86\u4e00\u4e2a\u6570\u5b66\u8bc1\u660e\uff0c\u91cc\u9762\u8c03\u4e86\u4e00\u5806lemma\uff0c\u53ef\u4ee5\u6e05\u6670\u7684\u8868\u8fbe\u51fa\u6211\u7684\u8bc1\u660e\u601d\u8def\uff0c\u8fd9\u79cd\u65b9\u5f0f\u5c31\u53ef\u4ee5\u88ab\u7528\u4e8e\u96f6\u77e5\u8bc6\u8bc1\u660e\u3002\u96f6\u77e5\u8bc6\u8bc1\u660e\u662f\u6307\uff1a\u5f53\u6211\u6709\u4e00\u4e2a\u5f88\u7cbe\u5999\u7684\u8bc1\u660e\uff0c\u6211\u4e0d\u60f3\u544a\u8bc9\u522b\u4eba\u6211\u7684\u8bc1\u660e\u601d\u8def\uff0c\u4f46\u6211\u60f3\u8ba9\u522b\u4eba\u77e5\u9053\u6211\u5df2\u7ecf\u8bc1\u660e\u4e86\u8fd9\u4e2a\u95ee\u9898\uff0c\u90a3\u8be5\u600e\u4e48\u529e\u5462\uff1f\u9996\u5148\uff0c\u6211\u4eec\u90fd\u77e5\u9053\u8fd9\u4e2a\u547d\u9898\u672c\u8eab\u662f\u4ec0\u4e48\uff0c\u8fd9\u4e2a\u547d\u9898\u672c\u8eab\u5e94\u8be5\u662f\u4e2a\u7c7b\u578b\u7b7e\u540d\uff0c\u547d\u9898\u662f\u7528\u7c7b\u578b\u7b7e\u540d\u8868\u8fbe\u7684\uff0c\u8fd9\u4e2a\u547d\u9898\u7684\u8bc1\u660e\u662f\u7b26\u5408\u7c7b\u578b\u7684\u4e00\u4e2a\u51fd\u6570\u4f53\uff0c\u4e00\u4e2a\u51fd\u6570\u4f53\u5c31\u662f\u4e00\u4e2a\u8868\u8fbe\u5f0f\uff0c\u4e00\u4e2a\u503c\uff0c\u4f46\u662f\u6211\u4e0d\u80fd\u628a\u5b83\u544a\u8bc9\u522b\u4eba\uff0c\u4e0d\u7136\u5176\u4ed6\u4eba\u5c31\u80fd\u770b\u51fa\u6211\u7684proof technique\uff08\u8bc1\u660e\u6280\u5de7\uff09\u3002\u6211\u600e\u4e48\u8ba9\u4f60\u77e5\u9053\u6211\u6709\u8fd9\u4e2a\u8bc1\u660e\u5462\uff1f\u6211\u53ef\u4ee5unfold\uff08\u89e3\u538b\u7f29\uff09\u8fd9\u4e2aproof\uff0c\u628a\u6240\u6709\u7684lemma\u5168\u90e8\u5c55\u5f00\u6210\u6700\u5e95\u5c42\u7684\u5f62\u5f0f\uff0c\u5f97\u5230\u4e00\u4e2a\u4e0aGB\u7ea7\u522b\u7684\u5de8\u578b\u8bc1\u660e\uff0c\u5b83\u53ef\u4ee5\u88ab\u673a\u5668check\u5b83\u7684\u6b63\u786e\u6027\uff0c\u4f46\u662f\u5bf9\u4eba\u7c7b\u6765\u8bf4\u6ca1\u6709\u53ef\u8bfb\u6027\uff0c\u5149\u662f\u4ece\u5934\u5230\u5c3e\u8bfb\u4e00\u904d\uff0c\u5c31\u8981\u82b1\u4e0a\u4e00\u4e2a\u6708\u7684\u65f6\u95f4\u3002<\/p>\n<p><strong>Q6:\u8fd9\u4e2a\u8fc7\u7a0b\u80fd\u5426\u88ab\u201c\u53cd\u7f16\u8bd1\u201d\u5462\uff1f<\/strong><\/p>\n<p><strong>ICE1000<\/strong><strong>\uff1a<\/strong>\u8fd9\u9700\u8981refold\uff08\u91cd\u65b0\u538b\u7f29\uff09\uff0c\u8fd9\u5f88\u660e\u663e\u662fundecidable\uff08\u4e0d\u53ef\u5224\u5b9a\u7684\uff09\u7684\uff0c\u4f8b\u5982\uff0c\u6211\u4eec\u60f3\u8c61\u4e00\u4e2a\u9012\u5f52\u51fd\u6570\uff0c\u9012\u5f52\u4e86100\u6b21\uff0c\u6211\u4eec\u662f\u6ca1\u6709\u529e\u6cd5\u53bb\u8ba9\u5b83\u56de\u5230\u521d\u59cb\u72b6\u6001\u7684\u3002\u800c\u6bcf\u4e00\u5c42\u6211\u4eec\u53c8\u53bb\u8c03\u7528\u4e86\u5f88\u591a\u522b\u7684\u9012\u5f52\u51fd\u6570\uff0c\u8fd9\u4e2a\u8fc7\u7a0b\u57fa\u672c\u65e0\u89e3\u4e86\u3002\u56e0\u6b64\u8fd9\u4ef6\u4e8b\u5728\u6570\u5b66\u4e0a\u662f\u6709\u5f88\u591a\u610f\u4e49\u7684\u3002<\/p>\n<p><strong>Q7:\u8bf7\u95ee\u60a8\u80fd\u518d\u8be6\u7ec6\u8bf4\u8bf4\u60a8\u5bf9\u6570\u5b66\u672c\u8eab\u7684\u770b\u6cd5\u5417\uff1f<\/strong><\/p>\n<p><strong>ICE1000<\/strong><strong>\uff1a<\/strong>\u6570\u5b66\u672c\u8eab\u5df2\u7ecf\u65e0\u6570\u6b21\u8bc1\u660e\u4e86\uff0c\u5373\u4f7f\u770b\u4f3c\u6ca1\u6709\u7528\u7684\u6570\u5b66\uff0c\u5b83\u603b\u5f52\u5728\u4e00\u4e2a\u65f6\u5019\u4f1a\u53d8\u5f97\u6709\u7528\u3002\u6b27\u62c9\u7814\u7a76\u7684\u795e\u79d8\u7684\u6570\u5b66\u7ed3\u6784\uff0c\u540e\u6765\u5bfc\u81f4\u4e86\u5f26\u8bba\u7684\u4ea7\u751f\u3002\u5728\u4ee3\u6570\u62d3\u6251\u5b66\u7814\u7a76\u7684\u7ea4\u7ef4\u4e1b\u4e4b\u7c7b\u7684\u7ed3\u6784\u73b0\u5728\u4e5f\u88ab\u7528\u5230\u4e86\u7269\u7406\u5b66\u4e2d\uff0c\u88ab\u4e0d\u88ab\u7528\u8d77\u6765\uff0c\u53ea\u662f\u4e00\u4e2a\u65f6\u95f4\u95ee\u9898\u800c\u5df2\u3002\u66f4\u6709\u8da3\u7684\u662f\uff0c\u6570\u5b66\u5728\u6ca1\u6709\u88ab\u7528\u8d77\u6765\u7684\u65f6\u5019\uff0c\u770b\u8d77\u6765\u4e00\u5b9a\u662f\u6ca1\u6709\u7528\u7684\u3002\u6240\u4ee5\u8bf4\u6211\u4eec\u5c31\u6ca1\u6709\u529e\u6cd5\u5728\u7814\u7a76\u6570\u5b66\u7684\u65f6\u5019\u8bc4\u4ef7\u5b83\u7684\u5b9e\u7528\u6027\u3002\u7eb5\u89c2\u5386\u53f2\uff0c\u53ea\u6709\u4e00\u4e2a\u4eba\u80fd\u505a\u5230\u5728\u7814\u7a76\u975e\u6570\u5b66\u9886\u57df\u65f6\u53d1\u660e\u6570\u5b66\u5de5\u5177\u53bb\u89e3\u51b3\u95ee\u9898\uff0c\u5176\u4ed6\u4eba\u90fd\u662f\u5229\u7528\u73b0\u6709\u7684\u6570\u5b66\u5de5\u5177\u89e3\u51b3\u95ee\u9898\u3002\u56e0\u6b64\uff0c\u6211\u4eec\u4e00\u5b9a\u8981\u5148\u628a\u6570\u5b66\u7814\u7a76\u5230\u5f53\u4e0b\u7684\u6781\u81f4\u3002\u4e5f\u6b63\u662f\u8fd9\u4e2a\u539f\u56e0\uff0c\u6211\u4e2a\u4eba\u8ba4\u4e3a\u7814\u7a76\u8f85\u52a9\u6570\u5b66\u7684\u610f\u4e49\u4e0d\u4e9a\u4e8e\u5f62\u5f0f\u5316\u9a8c\u8bc1\u3002\u5982\u679c\u7528\u7c7b\u578b\u7cfb\u7edf\u80fd\u628a\u5b83\u505a\u597d\uff0c\u5c31\u53ef\u4ee5\u89e3\u51b3\u6570\u5b66\u4e2d\u6700\u5927\u7684\u4e00\u4e2a\u75db\u70b9\uff1a\u4e00\u4e2a\u771f\u6b63\u7684\u6570\u5b66foundation\uff08\u57fa\u7840\uff09\u3002\u5b83\u4e0e\u96c6\u5408\u8bba\u4e0d\u540c\uff0c\u96c6\u5408\u8bba\u5176\u5b9e\u662f\u6211\u4eec\u5047\u88c5\u5728\u7528\u8fd9\u4e2afoundation\uff0c\u4f46\u5b9e\u9645\u4e0a\u8fd8\u662f\u50cf\u9ad8\u65af\u6216\u8005\u6b27\u62c9\u8fd9\u6837\u7684\u90a3\u79cd\u9760\u76f4\u89c9\u7684\u65b9\u5f0f\u53bb\u505a\u6570\u5b66\u3002\u90a3\u4e2a\u5e74\u4ee3\u7684\u6570\u5b66\u5bb6\uff0c\u90fd\u662f\u9760\u76f4\u89c9\u7684\uff1a\u6211\u8ba4\u4e3a\u4e09\u89d2\u5f62\u662f\u8fd9\u6837\u7684\uff0c\u90a3\u5c31\u662f\u8fd9\u6837\u7684\u3002\u4ed6\u4eec\u4e0d\u4f1a\u53bb\u60f3\u5e73\u9762\u51e0\u4f55\u5e94\u8be5\u57fa\u4e8e\u600e\u6837\u7684\u6846\u67b6\uff0c\u8b6c\u5982\u6b27\u51e0\u91cc\u5f97\u51e0\u4f55\u4e2d\u7684\u5e73\u884c\u7ebf\u6c38\u8fdc\u4e0d\u76f8\u4ea4\uff0c\u4e5f\u5c31\u662f\u7b2c\u4e94\u516c\u7406\u3002\u5fc5\u987b\u5f97\u5148\u5bf9\u516c\u7406\u8fdb\u884c\u89c4\u5b9a\uff0c\u4e4b\u540e\u624d\u80fd\u591f\u7528\u516c\u7406\u53bb\u8bc1\u660e\u4e09\u89d2\u5f62\u7684\u5185\u89d2\u52a0\u8d77\u6765\u662f180\u5ea6\u3002\u90a3\u4e9b\u6570\u5b66\u5bb6\u4eec\u4e0d\u4f1a\u58f0\u660e\u8fd9\u4e9b\u516c\u7406\u7684\u5b58\u5728\uff0c\u4ed6\u4eec\u53ea\u4f1a\u8bf4\u6211\u89c9\u5f97\u8fd9\u6837\u79fb\u52a8\u4e00\u4e0b\uff0c\u662f\u4e0d\u662f\u5c31\u8bc1\u660e\u4e86\u8fd9\u4e2a\u95ee\u9898\uff1f\u4f46\u662f\u4ed6\u4eec\u5176\u5b9e\u9690\u5f0f\u7684\u4f7f\u7528\u4e86\u4e00\u4e9b\u4e1c\u897f\u3002<img loading=\"lazy\" decoding=\"async\" class=\"aligncenter wp-image-2960 size-full\" src=\"https:\/\/sosconf.org\/wp-content\/uploads\/2020\/10\/michael-dziedzic-ir5gC4hlqT0-unsplash-scaled.jpg\" alt=\"\" width=\"2560\" height=\"2012\" srcset=\"https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-ir5gC4hlqT0-unsplash-scaled.jpg 2560w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-ir5gC4hlqT0-unsplash-300x236.jpg 300w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-ir5gC4hlqT0-unsplash-1024x805.jpg 1024w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-ir5gC4hlqT0-unsplash-768x604.jpg 768w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-ir5gC4hlqT0-unsplash-1536x1207.jpg 1536w, https:\/\/sosconf.cqu.org.cn\/wp-content\/uploads\/2020\/10\/michael-dziedzic-ir5gC4hlqT0-unsplash-2048x1609.jpg 2048w\" sizes=\"auto, (max-width: 2560px) 100vw, 2560px\" \/><br \/>\n\u200b\u5728\u8fd9\u91cc\u6211\u60f3\u804a\u804a\u6570\u5b66\u57fa\u7840\uff1a\u6570\u5b66\u57fa\u7840\u662f\u4e00\u79cd\u6982\u5ff5\uff0c\u8b6c\u5982\u5e0c\u5c14\u4f2f\u7279\u81ea\u7136\u6f14\u7ece\u3001 ZFC\uff0c\u5b83\u7684\u610f\u4e49\u5728\u4e8e\u63d0\u4f9b\u4e86\u4e00\u4e2a\u8ba8\u8bba\u6570\u5b66\u7684\u6846\u67b6\uff0c\u6570\u5b66\u754c\u5c06\u6570\u5b66\u57fa\u7840\u8bbe\u8ba1\u4e86\u51fa\u6765\uff0c\u4f46\u662f\u5728\u4f7f\u7528\u65f6\u5374\u8fd8\u662f\u51ed\u76f4\u89c9\u51fa\u53d1\uff1a\u6bd4\u5982\u4ed6\u4eec\u773c\u4e2d\u7684\u51fd\u6570\u8fd8\u53ea\u662f\u4e00\u4e2a\u516c\u5f0f\uff0c\u800c\u4e0d\u662f\u4e00\u4e2a\u7b1b\u5361\u5c14\u79ef\u7684\u5b50\u96c6\u3002\u6570\u5b66\u57fa\u7840\u5f3a\u8feb\u6211\u4eec\u601d\u8003\u8ba8\u8bba\u6570\u5b66\u65f6\u6700\u6700\u57fa\u7840\u7684\u5047\u8bbe\u3002\u800c\u7c7b\u578b\u8bba\u4f5c\u4e3a\u6570\u5b66\u57fa\u7840\uff0c\u6253\u5f00\u4e86\u8ba1\u7b97\u673a\u4e16\u754c\u7684\u5927\u95e8\uff0c\u7ed9\u4e86\u6211\u4eec\u00a0\u201c\u4e0e\u8ba1\u7b97\u673a\u8ba8\u8bba\u6570\u5b66\u201d \u7684\u673a\u4f1a\u3002\u4e3a\u4ec0\u4e48\u8fd9\u4e2a\u673a\u4f1a\u5982\u6b64\u91cd\u8981\u5462\uff1f\u56e0\u4e3a\u8ba1\u7b97\u673a\u53ef\u4ee5\u6bd4\u4eba\u7c7b\u66f4\u5feb\u66f4\u51c6\u786e\u5730\u68c0\u67e5\u8fd9\u4e9b\u5b9a\u4e49\u548c\u8bc1\u660e\u7684\u6b63\u786e\u6027\uff0c\u800c\u4e14\u5982\u679c\u8bc1\u660e\u6709\u95ee\u9898\uff0c\u5b83\u8fd8\u53ef\u4ee5\u63d0\u793a\u4eba\u7c7b\u54ea\u91cc\u6709\u95ee\u9898\u3002\u7f3a\u70b9\u5c31\u662f\u4f60\u9700\u8981\u544a\u8bc9\u8ba1\u7b97\u673a\u51e0\u4e4e\u6240\u6709\u7684\u8bc1\u660e\u7ec6\u8282\uff0c\u4f46\u662f\u8fd9\u53c8\u53ef\u4ee5\u501f\u52a9\u4e00\u4e9b\u53eb\u505a proof engineering \u7684\u624b\u6bb5\u89e3\u51b3\u3002\u800c\u7814\u7a76\u7c7b\u578b\u8bba\u672c\u8eab\u7684\u610f\u4e49\u5c31\u5728\u4e8e\u4fee\u6539\u5b83\uff0c\u4f7f\u5b83\u53d8\u5f97\u66f4\u597d\u7528\u3001\u80fd\u66f4\u76f4\u89c2\u5730\u8868\u8fbe\u6570\u5b66\u7ed3\u6784\u3002\u5c31\u50cf\u6570\u5b66\u57fa\u7840\u53ef\u4ee5\u88ab\u4fee\u6539\u4e00\u6837\u3002\u6bd4\u5982\u8bf4\u6211\u628a\u6b27\u51e0\u91cc\u5f97\u51e0\u4f55\u5e73\u884c\u7ebf\u5747\u7ebf\u6c38\u8fdc\u4e0d\u76f8\u4ea4\u4fee\u6539\uff0c\u4e24\u6761\u5e73\u884c\u7684\u76f4\u7ebf\uff0c\u6709\u53ef\u80fd\u76f8\u4ea4\u4f1a\u600e\u4e48\u6837\u5462\uff1f\u6709\u4e09\u89d2\u5f62\u4e09\u4e2a\u5185\u89d2\u52a0\u8d77\u6765\u4e0d\u7b49\u4e8e180\u5ea6\u662f\u600e\u6837\u7684\uff1f\u6211\u4eec\u5f97\u5230\u4e86\u975e\u6b27\u51e0\u4f55\uff0c\u6211\u4eec\u8fd8\u5f97\u5230\u4e86\u9ece\u66fc\u51e0\u4f55\uff0c\u5c31\u6709\u4e86\u4e0d\u4e00\u6837\u7684\u6570\u5b66\u3002\u5f53\u6211\u4eec\u5728\u7814\u7a76\u51e0\u4f55\u56fe\u5f62\u7684\u65f6\u5019\uff0c\u6211\u4eec\u5047\u8bbe\u4e0d\u5173\u5fc3\u957f\u5ea6\uff0c\u4e0d\u5173\u5fc3\u5927\u5c0f\uff0c\u4e0d\u5173\u5fc3\u76f4\u7684\u8fd8\u662f\u5f2f\u7684\uff0c\u6211\u4eec\u53ea\u5173\u5fc3connectivity\uff08\u8fde\u901a\u6027\uff09\uff0c\u6bd4\u5982\u8bf4\u4e24\u6761\u770b\u8d77\u6765\u4e0d\u4e00\u6837\u7684\u76f4\u7ebf\uff0c\u6211\u4eec\u8ba4\u4e3a\u5b83\u4eec\u662f\u4e00\u6837\u7684\u3002\u8fdb\u4e00\u6b65\u5730\uff0c\u6211\u4eec\u53ef\u4ee5\u7814\u7a76\u66f4general\u7684\u6027\u8d28\uff1a\u6bd4\u5982\u7814\u7a76\u4e00\u4e2a\u7ebf\u6bb5\uff0c\u4e00\u4e2a\u70b9\uff0c\u53ef\u4ee5\u6709\u70b9\u4e0e\u70b9\u4e4b\u95f4\u7684\u7ebf\u6bb5\u5417\uff1f\u7ebf\u6bb5\u4e0e\u7ebf\u6bb5\u4e4b\u95f4\u53ef\u4ee5\u6709\u7ebf\u6bb5\uff0c\u4e5f\u5c31\u662f\u9762\u3002\u6211\u4eec\u8fd8\u53ef\u4ee5\u628a\u4e00\u4e2a\u7ebf\u6bb5\u7684\u5de6\u53f32\u70b9\u548c\u4ed6\u81ea\u5df1\u8fde\u8d77\u6765\uff0c\u6211\u4eec\u4e5f\u53ef\u4ee5\u628a\u5b83\u505a\u4e24\u70b9\u5148\u8f6c\u8fc7\u6765\uff0c\u5f97\u5230\u4e86\u83ab\u6bd4\u4e4c\u65af\u73af\uff0c\u7136\u540e\u6211\u4eec\u8fd8\u53ef\u4ee5\u8ba9\u4e00\u4e2a\u70b9\u53ef\u4ee5\u7ed5\u7740\u4e00\u4e2a\u5706\u8f6c\u3002\u6211\u4eec\u8fd8\u53ef\u4ee5\u628a\u4e00\u4e2a\u5706\u7ed5\u7740\u4e00\u4e2a\u5706\u8f6c\uff0c\u8fd9\u5f97\u5230\u4e86\u4ec0\u4e48\uff1f\u5f97\u5230\u751c\u751c\u5708\uff0c\u751c\u751c\u5708\u662f\u4e00\u4e2a\u5f88\u7ecf\u5178\u7684\u62d3\u6251\u7ed3\u6784\uff0c\u56e0\u4e3a\u5b83\u540c\u6784\u4e8e\u4e24\u4e2a\u5706\u5708\u4e0a\u7684\u70b9\u7684\u5730\u65b9\uff0c\u8fd9\u4e2a\u540c\u6784\u5173\u7cfb\u7528HoTT\uff08\u540c\u4f26\u7c7b\u578b\u8bba\uff09\u5199\u7684\u975e\u5e38\u76f4\u89c2\uff0cHoTT\u6bd4\u8d77\u4f20\u7edf\u7c7b\u578b\u7684\u610f\u4e49\uff0c\u5c31\u5728\u4e8e\u5b83\u4f7f\u5f97\u63cf\u8ff0\u8fd9\u79cd\u8fde\u7eed\u7684\u7ed3\u6784\uff0c\u5305\u62ec\u751c\u751c\u5708\u5706\u5708\uff0c\u8fd9\u79cd\u4e1c\u897f\u53d8\u5f97\u975e\u5e38\u65b9\u4fbf\uff0c\u5728\u8ba1\u7b97\u673a\u4e2d\u975e\u5e38\u65b9\u4fbf\uff0c\u6240\u4ee5\u6211\u5728\u8ba1\u7b97\u673a\u4e2d\u53ef\u4ee5\u8868\u8fbe1\u4e2a\u751c\u751c\u5708\uff0c\u56e0\u4e3a\u751c\u751c\u5708\u5c31\u662f1\u4e2a\u67094\u4e2a\u6784\u9020\u51fd\u6570\u76841\u4e2a\u7c7b\u578b\u3002\u5c31\u5982\u524d\u9762\u6240\u8bf4\u7684\uff0c\u6570\u5b66\u4e00\u5b9a\u8981\u53d1\u5c55\u5f97\u66f4\u5feb\uff0c\u8fd9\u6837\u624d\u80fd\u591f\u6700\u597d\u5730\u53bb\u89e3\u51b3\u5176\u4ed6\u95ee\u9898\u3002\u7136\u540e\u624d\u8bf4\u4eba\u4eec\u4e00\u5b9a\u4f1a\u89c9\u5f97\u6570\u5b66\u6709\u7528\u3002\u5982\u679c\u7814\u7a76\u6570\u5b66\u662f\u6709\u7528\u7684\uff0c\u90a3\u4e48\u89e3\u51b3\u6570\u5b66\u7684\u95ee\u9898\u5c31\u4e00\u5b9a\u662f\u6709\u7528\u7684\uff0c\u6240\u4ee5\u7c7b\u578b\u7cfb\u7edf\u5c31\u662f\u503c\u5f97\u7814\u7a76\u7684\uff0c\u8ba9\u6211\u89c9\u5f97\u53ef\u4ee5\u53bb\u641e\u4e00\u641e\uff0c\u5176\u6b21\u662f\u8fd9\u4e2a\u4e1c\u897f\u53ef\u4ee5\u5e2e\u52a9\u4f60\u7f16\u7a0b\uff0c\u5bf9\u4e8e\u5199\u4ee3\u7801\u672c\u8eab\u4e5f\u5f88\u6709\u610f\u4e49\u3002<\/p>\n<p><strong>Q8:<\/strong><strong>\u8bf7\u95ee\u5c31\u60a8\u81ea\u5df1\u800c\u8a00\uff0c\u5f00\u6e90\u4e3a\u60a8\u5e26\u6765\u4e86\u4ec0\u4e48\u5462\uff1f<\/strong><\/p>\n<p><strong>ICE1000<\/strong><strong>\uff1a<\/strong>\u5f00\u6e90\u7684\u98ce\u6c14\u5f71\u54cd\u4e86\u5b66\u672f\u793e\u533a\uff0c\u6240\u4ee5\u5927\u5bb6\u4e5f\u503e\u5411\u4e8e\u5206\u4eab\u4ee3\u7801\u3002\u53e6\u5916\u5f00\u6e90\u793e\u533a\u5f62\u6210\u4e86\u4e00\u4e9b\u4e0d\u6210\u6587\u7684\u5171\u8bc6\uff0c\u8fd9\u4f7f\u5f97\u6211\u4eec\u8fd9\u4e9b\u73a9\u5c0f\u4f17\u6280\u672f\u7684\u4eba\u7ba1\u7406\u548c\u7ef4\u62a4\u81ea\u5df1\u7684\u793e\u533a\u4e5f\u53d8\u5f97\u5f88\u65b9\u4fbf\u4e86\u3002\u5728\u6211\u7684\u5b66\u4e60\u65e9\u671f\u6211\u501f\u52a9\u90a3\u4e2a\u5565\u5565\u5565 Hub \u5b66\u5230\u4e86\u5f88\u591a\u59ff\u52bf\uff0c\u540e\u6765\u6211\u5728\u6280\u672f\u6bd4\u8f83\u6210\u719f\u7684\u65f6\u5019\u4e5f\u53cd\u54fa\u4e86\u793e\u533a\uff0c\u6ca1\u6709\u5f00\u6e90\u7684\u98ce\u6c14\u8fd9\u4e9b\u90fd\u662f\u65e0\u6cd5\u505a\u5230\u7684\u3002<\/p>\n<p><strong>Q9<\/strong><strong>:\u8bf7\u95ee\u60a8\u8fd8\u60f3\u5bf9\u8bfb\u8005\u8bf4\u4e00\u4e9b\u4ec0\u4e48\u5462\uff1f<\/strong><\/p>\n<p><strong>ICE1000<\/strong><strong>\uff1a<\/strong>\u5e0c\u671b\u5927\u5bb6\u4fdd\u6301\u5bf9\u5199\u4ee3\u7801\u7684\u70ed\u7231\u575a\u6301\u4e0b\u53bb\u5427\uff0c\u5f00\u6e90\u793e\u533a\u8fd9\u79cd\u51e0\u4e4e\u5b9e\u73b0\u4e86\u5171\u4ea7\u4e3b\u4e49\u7684\u5c0f\u578b\u793e\u4f1a\u4ec5\u5b58\u4e8e\u6280\u672f\u5708\u5b50\uff0c\u662f\u6211\u4eec\u7f16\u7a0b\u7231\u597d\u8005\u4eec\u7684\u9a84\u50b2\u3002\u540c\u65f6\u4e5f\u5e0c\u671b\u5927\u5bb6\u4e5f\u80fd\u4e3a\u5f00\u6e90\u4e16\u754c\u7684\u7e41\u8363\u5c3d\u81ea\u5df1\u7684\u4e00\u4efd\u529b\uff0c\u4fdd\u6301\u8c26\u900a\u548c\u53cb\u5584\uff0c\u5f00\u6e90\u9879\u76ee\u7684\u7ef4\u62a4\u8005\u4e5f\u90fd\u662f\u666e\u901a\u4eba\uff0c\u6211\u4eec\u4eab\u53d7\u4e86\u522b\u4eba\u7684\u4ed8\u51fa\u4e5f\u5e94\u8be5\u5c0a\u91cd\u4ed6\u4eec\u624d\u5bf9\u3002<\/p>\n<p>&nbsp;<\/p>\n<p>#\u672c\u6b21\u4e13\u8bbf\u7ed3\u675f#<\/p>\n<p>&nbsp;<\/p>\n<p><strong>\u4ee5\u4e0b\u901a\u4fe1\u65b9\u5f0f\u4e3a\u5b66\u751f\u5f00\u6e90\u5e74\u4f1a\u7684\u5b98\u65b9\u8054\u7edc\u65b9\u5f0f\uff0c\u656c\u8bf7\u5173\u6ce8\u3002<\/strong><\/p>\n<p>\u672c\u6b21\u6d3b\u52a8\u5b98\u65b9\u7f51\u7ad9:\u00a02020zh.sosconf.org<\/p>\n<p>\u5b66\u751f\u5f00\u6e90\u5e74\u4f1a\u5b98\u65b9\u7f51\u7ad9: sosconf.org<br \/>\n\u7535\u62a5\u82f1\u6587\u7fa4\u7ec4\uff1ahttps:\/\/t.me\/sosconf<br \/>\n\u5b98\u65b9\u5fae\u535a\uff1ahttps:\/\/weibo.com\/sosconf<br \/>\n\u7535\u62a5\u4e2d\u6587\u7fa4\u7ec4\uff1ahttps:\/\/t.me\/soscon<br \/>\n\u4e2d\u6587\u4ea4\u6d41QQ\u7fa4\uff1a738852894<\/p>\n<p>\u5fae\u4fe1\u516c\u4f17\u53f7\uff1a\u5b66\u751f\u5f00\u6e90\u5e74\u4f1a<\/p>\n","protected":false},"excerpt":{"rendered":"\u672c\u6b21\u4e13\u8bbf\u4e3a\u6b64\u6b212020\u4e2d\u6587\u5b66\u751f\u5f00\u6e90\u5e74\u4f1a\u7cfb\u5217\u4e13\u8bbf\u552f\u4e00\u7684\u7ebf\u4e0b\u4e13\u8bbf\uff0c\u53d7\u8bbf\u8005\u5343\u91cc\u51b0\u5c01\/ICE1000\uff08\u4ee5\u4e0b\u4ee5\u201c\u51b0\u51b0\u201d\u7b80\u79f0\uff09\u4e0d\u4ec5\u5e26\u6765\u4e86\u8fd9\u671f\u8d28\u91cf\u6781\u9ad8\u7684\u8bbf\u8c08\uff0c\u540c\u65f6\u4e5f\u4f5c\u4e3a\u4e00\u4f4d\u201c\u6210\u90fd\u571f\u8457\u201d\uff0c\u5e26\u9886\u7b14\u8005\u6e38\u89c8\u4e86\u8bb8\u591a\u6210\u90fd\u5e02\u4e2d\u5fc3\u9c9c\u4e3a\u4eba\u77e5\u7684\u597d\u53bb\u5904\u3002","protected":false},"author":9,"featured_media":2955,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[51],"tags":[158,70,159,157,156],"class_list":["post-2953","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-blog","tag-158","tag-chengdu-zh-hans","tag-sosconf-zh-zh-hans","tag-157","tag-156"],"_links":{"self":[{"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/posts\/2953","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/users\/9"}],"replies":[{"embeddable":true,"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/comments?post=2953"}],"version-history":[{"count":16,"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/posts\/2953\/revisions"}],"predecessor-version":[{"id":3048,"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/posts\/2953\/revisions\/3048"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/media\/2955"}],"wp:attachment":[{"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/media?parent=2953"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/categories?post=2953"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/sosconf.org\/zh-hans\/wp-json\/wp\/v2\/tags?post=2953"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}