Thats the neat part. We won't.

Say more. Is the API access unlimited? What models are available?

It's unlimited for the models that have unlimited use in GitHub Copilot, gpt-4.1.

You are not crazy. Logic programming is the future

I know this is useful for crypto, but I think think I'm actually more interested in what new modes of remote code running on untrusted platforms this enables.

That is exactly the reason it's useful for crypto, nodes need to verify the output of code running on other nodes without trusting them.

This scheme in particular is not useful for cryptocurrencies; we already knew how to make efficient zkSNARKs with perfect zero-knowledge before this result. This paper is a beautiful work of theory.

It does seem like the article touches on concerns relevant to homomorphic encryption. Maybe someone knows if there is a connection.

I think it was just a genetic algorithm.

I would be interested in reading more if you manage to find the paper(s).

This reminds me of a section from a category theory text that I encountered.

It had similarly 'crazy' what-ifs, including one where the author used the quadratic formula and interpreted some meaning from it.

It was a course only text, not distributed outside the university as far as I know.

I'm having a lot of fun with this tutorial. Has anyone done anything interesting with these meta compilers for projects?

A couple of metacompiler experiments with Lua and Haskell, https://loup-vaillant.fr/projects/metacompilers/

Wow. What a quality tool. Thanks for sharing!

Author here - thank you for the compliment! Always happy to answer any questions (the docs are admittedly quite sparse) and hear about what people like/dislike about the library!

Python's Deal library provides contracts and a small portable formal proofs area of the codebase.

Additionally, Deal integrates with CrossHair which does concolic execution of the tests and functions annotated with contracts. It's integrated with Z3, and most of the Python primitives are covered.

It just works surprisingly well for incrementally building up provable code properties.

Thank you! This is great, sounds like what I'm looking for.

I'm also curious about your experiences using nim as a secret weapon in corporate programming.

I refer you to my post on the Nim 2.0 release:

https://news.ycombinator.com/item?id=36956144