Formalizing 100 Theorems

https://www.cs.ru.nl/~freek/100/

還是benchmark好。一翻兩瞪眼，誰都沒話講。

c,cpp,java,python,js,swift/objectiveC
還就是cpp模板有希望做這種題。講haskell的一些現存軟件翻譯下也許就可以了。

例如說，下面這個資料，我認為沒什麼翻譯困難（此論點請cpp專家批評指正）。https://cs.pomona.edu/~kim/CSC181S16/docs/TOTP.pdf

這種東西，到不一定要CPP，連C都不需要。最好的是domain specific language。

還有coq不是oCaml寫的嗎？那裏來的一定要CPP模板這個說法的？
【 在 chebyshev (......) 的大作中提到: 】
: https://www.cs.ru.nl/~freek/100/
: 還是benchmark好。一翻兩瞪眼，誰都沒話講。
: c,cpp,java,python,js,swift/objectiveC
: 還就是cpp模板有希望做這種題。講haskell的一些現存軟件翻譯下也許就可以了。
: 例如說，下面這個資料，我認為沒什麼翻譯困難（此論點請cpp專家批評指正）。
: https://cs.pomona.edu/~kim/CSC181S16/docs/TOTP.pdf

其他那些系統不是第一層的語言。維護成謎，用戶不多。
cpp那些歪七扭八塞進去的所謂features，在第一層語言裡是異數。看著像大牛燒錢幹
私活。

我剛查了下，確實有人將haskell翻譯成cpphttps://www.vandenoever.info/blog/2015/07/12/translating-haskell-to-c++.html

【 在 netghost (Up to Isomorphism) 的大作中提到: 】
: 這種東西，到不一定要CPP，連C都不需要。最好的是domain specific language。
: 還有coq不是oCaml寫的嗎？那裏來的一定要CPP模板這個說法的？

問題是這種formal proof本來就是小衆，追求用戶多也沒什麼用吧。

【 在 chebyshev (......) 的大作中提到: 】
: 其他那些系統不是第一層的語言。維護成謎，用戶不多。
: cpp那些歪七扭八塞進去的所謂features，在第一層語言裡是異數。
: 我剛查了下，確實有人將haskell翻譯成cpp
: https://www.vandenoever.info/blog/2015/07/12/translating-haskell-to-c++.
html

此類項目確實是小眾的。但時間上，此類項目之持久力驚人。
第一個圖靈獎就是定理機器證明。

此領域的一個問題是其工具在時間上沒有持續性。
過幾年就有個不同觀點的系統出來。導致軟件很難積累。

【 在 netghost (Up to Isomorphism) 的大作中提到: 】
: 問題是這種formal proof本來就是小校非笥脩舳嘁矝]什麼用吧。
: html