Writing a C Compiler (2017)

Re:Writing a C Compiler (2017) by JonChesterfield on Friday June 09, 2023 @10:11AM (#36258069)

I've seen it claimed that ML was originally written, in lisp, in order to have a better language to write compilers in.

[ Parent | on HN ]

Re:Writing a C Compiler (2017) by lispm on Friday June 09, 2023 @01:06PM (#36260806)

ML was written as the language used by the theorem prover LCF. It was written in Lisp.

[ Parent | on HN ]

Re:Writing a C Compiler (2017) by JonChesterfield on Friday June 09, 2023 @08:51PM (#36266400)

I didn't know that link, searches seem to confirm. Thank you.

The LCF style provers rely on the host language type system. A theorem instance can only be created by the trusted kernel. Lisp doesn't obviously lend itself to that - you could represent the proof, but I'm not clear how you'd prevent forging one.

[ Parent | on HN ]