Global Feed Post Login
Replying to f6XF

[1/3] 我本来是不会写 Python 的,但现在赶鸭子上架也能写点儿了,毕竟每月付给我两千欧元(然后我只花了一小半时间在工作上)。我现在只会写单个 Python 3 脚本,并且只引用 Python 标准库。我把 Python 解释器当做一个代码执行的平台,就是说但凡编译期能固定下来的数据都用 Lisp 代码把这些数据直接输出到 Python 文件里作为全局列表,然后 Python 代码启动后第一件事就是在内存里建一个 SQLite 数据库把所有数据狠狠地插进去,接下来的计算尽可能地用 SQL 查询来表达,SQL 语句和正则表达式都可以在 Lisp 代码里完成开发调试,然后直接拿到 Python 下面去用也不会错。我只能说凑合着用吧……

29
f6XF 1y ago

[1/3] 书上一个不起眼的引理,卡了我一个半月,证明写了一千多行代码还没写到一半。然后其中有个关键步骤,又卡了我一个多星期,直到刚才才终于拨云见日,但要想完成它还要再写很多代码。形式化证明的繁重工作量,在一般情况下是无法避免的(少数情况下才可以自动推理)。 ​​​

Reply to this note

Please Login to reply.

Discussion

No replies yet.