I tried setting up an F* development environment on a Mac…

Yeah, that’s the rant. You can probably guess how it went…

Ah yes, the olde issue with using something not a lot of people use.

What are you working on with F*, btw? I'm an avid user of Why3, will probably migrate to F* eventually.

That language sounds interesting. I wanted to look up example code but wtf I can’t find anything. Not even a hello world. I’m really confused now.

@RememberMe I kinda did figure there could’ve been an issue somewhere on the road. A bit less so since I have a F* dev env nicely setup on my linux machine. Turns out the version of z3 that F* is essentially married to is incompatible with at least the current MacOS version.

At this time I wanted to see if I could leverage F* to come up with a correctness-proofed version of an algorithm we didn’t really get just right during a hackthon some time ago. So just for fun as I had time to spare.

@Lensflare there’s F* code out there. But yeah, I don’t think you’ll find a hello world example for a lang that’s meant for program verification…

Why are you shit talking others people code?
AT Least use the full word Fuck, Fucking Fuckers
(joke)

@RememberMe also your Why3 rant kind of inspired this effort :D I had been saving further studies on F* for later but you got me going: why not now?

I had to resign to just running it on Linux

@whyreadthis looks like that’s what I’ll have to as well. There’s of course the option of running F* in a Docker container, but I’m not a fan of using Emacs in the terminal, so it’s still more pain than it’s worth.