News for hackers. Stuff that matters.

A comment on The Deep Link Equating Math Proofs and Computer Programs.

Re:The Deep Link Equating Math Proofs and Computer Programs by throwthrow5643 on Thursday October 12, 2023 @08:16AM (#37856144)
How to formally verify a single page web application?
[ Parent | on HN ]
Re:The Deep Link Equating Math Proofs and Computer Programs by mdnahas on Thursday October 12, 2023 @12:42PM (#37859580)
Write the code and proofs in Coq. Coq can output OCaML. I believe OCaML can compile to JavaScript.

That will allow you to verify the pure functions. It will not verify the input/output that will also be necessary.

[ Parent | on HN ]
Re:The Deep Link Equating Math Proofs and Computer Programs by Warwolt on Thursday October 12, 2023 @01:59PM (#37860610)
Depends on the properties you want to verify
[ Parent | on HN ]