it is very much a related idea. an `assert` statement in e.g. `python` is a statement your code is making about what it means to be correct, and furthermore a statement about what conditions would have to exist to validate the first statement: for example you might need to run it with certain inputs, on a certain file or kind of file.

`lean4` is very much about the same two ideas. you can make statements about what it means for the code to say something interesting, usually something relevant to whether or not it's correct, and you make statements about the circumstances in which you would evaluate that.

people are interested in `lean4` because it allows you to make more interesting statements of both kinds, and you have tools to be much more specific about the details, the `assert` statements in `python` can't really call each other for example, they don't really compose. in `lean4` the ability to compose such statements is very important.

but you can write regular programs in it too. this is a reverse proxy faster than `nginx`: https://cdn.s4.gl/serve-fd.lean