Zulip Chat Archive

Stream: new members

Topic: should I formalize WASM instead?

Huỳnh Trần Khanh (Jun 11 2021 at 04:29):

I'm trying to reason about competitive programming programs. I can't directly express the algorithms in Lean because the limited semantics make it hard to express memory reuse and other tricks that make the programs efficient. My original idea was to formalize a restricted subset of C++, however after a while I realized that this might be overkill. Is it a good idea to use WASM as a language to express imperative algorithms?

Huỳnh Trần Khanh (Jun 11 2021 at 04:31):

If you don't know what competitive programming is, this page is full of competitive problems: https://cses.fi/problemset/list/. The https://usaco.guide page also provides a good introduction.

Yakov Pechersky (Jun 11 2021 at 04:31):

How about LLVM?

Huỳnh Trần Khanh (Jun 11 2021 at 04:33):

Ease of formalization should also be considered, LOL. LLVM IR is a humongous language.

Huỳnh Trần Khanh (Jun 11 2021 at 04:34):

Competitive programming programs don't do much I/O aside from reading and writing to standard streams.

Huỳnh Trần Khanh (Jun 11 2021 at 04:34):

So far, WASM seems like a promising candidate but I want experts to weigh in too.

Mario Carneiro (Jun 11 2021 at 04:45):

Why not formalize IMP or lisp instead? Something semi-practical but with a small basis so you can prove properties

Mario Carneiro (Jun 11 2021 at 04:46):

almost any real world language will have way too many moving parts for your needs

Last updated: Dec 20 2023 at 11:08 UTC