solomonb

The natural numbers are countably infinite. For each n ∈ ℕ, there is a proof by reflexivity that n = n. Hence there are countably infinitely many such proofs, one for each natural number.

Continuing to develop my LPFM radio station www.kpbj.fm

- We have accumulated almost all the equipment needed to setup our FM broadcast. The main piece of equipment we still need is the EAS Decoder.

- Our studio space build is in progress. I recently welded some tables for the booth and found an old Orban Optimod for our airchain.

- We have over 80 shows and our roster continues to grow.

If you are in Los Angeles or love community radio please reach out.

Did you have previous experience with formal verification and/or dependent types?

But CNC machining still requires a ton of physical skills. Its true that you maybe aren't planning out and executing every single tool pass by hand but there is still a tremendous amount of knowledge and physical skill that goes into setting up, indicating parts, etc.

okay maybe i was wrong about them being technically endangered, i misread that somewhere. Still doesn't change the fact that we shouldn't be abusing animals to have pseudo-intellectual psychedelic experiences.

Can we please leave the fucking toads alone?

This is an endangered species getting massively abused by the wellness "shaman" industry. It fucking sucks. Just use synthetic 5me0-dmt if you really must do a goofy vision quest larp.

I am responding to a comment that is framing the reduced size as a good thing from an obesity perspective...

Is obesity more or less prevalent now versus 1991?

The churn in this space puts javascript to shame. As an example, its only been a few months and AFAICT no one is even talking about openclaw anymore.

Waiting for the remaining broadcast equipment for my LPFM (www.kpbj.fm) to arrive! Then we finally get on the broadcast band. We have over 80 shows at this point. We still need fundraising support. If you are in Los Angeles and want to support freeform community please reach out.

Now I want a hat with the Agnostic Front logo but that says Pareto Front.

I agree that Lean or any of the other languages I listed would be a better choice then Idris and despite how I wrote my original post I wouldn't recommend Idris to someone who explicitly wanted a theorem prover.

Idris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc.

It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.

Correct. There are awful tricks to write [1] dependent Haskell but even then it isn't powerful enough and has a significantly worse user experience then a proper dependently typed proof checker (as bad as the UX is on those!).

That said there are other languages such as Agda, Idris, and Rocq that would be fantastic replacements to Lean, especially if you care about staying constructive.

1. https://homepages.inf.ed.ac.uk/slindley/papers/hasochism.pdf

I find that claude rarely uses its memories.

My experience talking with high level mathematicians is that they tend to know their subjects so well and are so excited to share it that they can and will scale their explanation to match their audience.

Thank you for creating Recurse! I had an incredible experience at RC in 2019. I still have friends from my batch.

I deeply wish I had time to do it again.

They offer recruiting services.

I'm reading The Drowned World right now. Incredible book, highly recommended.

To be fair the original commenter was incredibly snarky.

The integer `1` can mean whatever you want, it doesn't need to be a cent. Haskell's `Fixed` type is a good example of this:

https://hackage-content.haskell.org/package/base-4.22.0.0/do...

Its a wrapper around an `Integer` where you declare the scale in the type. So if you use `Fixed E2` as your type then `MkFixed 1` is 1 cent. If you did `Fixed E3` as your type then `MkFixed 1` is 0.1 cent. In both cases it is entirely an integer encoding.

Getting to discover Oleg Kiselyov's work for the first time is such a treat. His web archive is incredible! I'm envious of the author and anyone else discovering it today.

https://okmij.org/ftp/

There was another project I saw years ago that this reminds me of. It was a guy who had been running a simulated city/community for like 20 years. The whole thing was done on pen and paper and used complex rule system he had devised. Similar pre-internet outsider art vibe.

The modern equivalant is the all-in-one karaoke machine :)

The current tenants will see the listing for the vacant unit.

You're absolutely right!

They don't make them like they used to

Messing around with my Lambda Calculus tutorial repo. I just did a total rewrite of Nominal Inductive Types.

https://github.com/solomon-b/lambda-calculus-hs

Interesting! The rules for AM carrier current appear to be more similar to the FM rules, that is they are based on field strength readings that result in a roughly 200ft range.

There is probably a bunch of subtlety about where you measure from as your antenna could be quite large.

To my knowledge there is no legal way to do unlicensed carrier current transmission. Do you have information otherwise? I've always wanted to try it..

The Part15 regulations for AM and FM are more subtle then what you present here. On FM it is based on field strength readings, the exact values of which escape me, but yielding roughly the range you describe.

For AM the rules are more interesting. You can have up to a 3m antenna length and 100mW of DC power input to the final stage of amplification. The optimal setup is a class E amplifier with ~95-99% efficiency into a properly grounded 3m base loaded vertical antenna. The antenna will be grossly undersized but you try to compensate with a huge loading coil. In ideal conditions this setup can get you about 0.5km range.

LPFM is a much more significant undertaking and it is not trivial to get an LPFM license. I know because I have one :)