如何形式化验证一场技术面试 完整代码可见https://github.com/KonjacSource/NQueens. 标题捏自https://aphyr.com/posts/342-typing-the-technical-interview, 这里有一篇中文翻译https://zhuanlan.zhihu.com/p/84634204, 不会写小作文, 所以只偷个名字😢. 本文意图展示一下如何确保正确性地编写 2024-06-24 #编程 #计算机 #Agda #形式验证
如何浪费青春 社交和酒精都有成瘾性 -- 我说的 2023年秋末的一个夜晚, 我在学校附近散步, 路遇酒吧一条街. 请求酒鬼同学带我去, 去了. 浪费时间了, 遇到一个女人了, 她看上我了, 我觉得她有点胖, 并且不太好看, 但我喝多了, 她拉我去开房, 我虽然有些不情愿, 但没有拒绝, 那天晚上我在床上确诊阳痿了, 一夜过后, 处身依旧. 次日她走了之后就不再 2024-06-11 #杂谈
写给一般计算机人的Lean4安利 本文主要给有计算机背景(起码懂一门强类型编程语言, 如果读者懂函数式编程或者 Rust 就更好了)的人介绍一下 Lean4 (作为一个编程语言而不是证明助手). 环境配置不在本文介绍范围内, 请参考https://lean-lang.org/lean4/doc/setup.html或者参考这里https://zhuanlan.zhihu.com/p/656770107. 另外由于 Mark 2023-11-25 #编程 #计算机 #Lean
类型体操指北 (Haskell) 作为类型系统最复杂的非DT语言之一, Haskell有着强大的类型编程能力. 我们将从最简单的构造开始展示这些能力, 本文假定读者了解Haskell的基本语法. 本文使用的版本是GHC 9.0.2, 但在较旧的版本上这些代码也能运行. 首先我们需要打开以下拓展 12345678910{-# LANGUAGE MultiParamTypeClasses #-}{ 2023-11-08 #Haskell #编程 #计算机