> They are often misrepresented presented as a futile toy for “galaxy-brain people”, providing no benefit to the regular programmer
Me: Go on I am listening...
> The backend I’m writing is just a program — written in Haskell — that takes as input the internal representation of Agda programs, and outputs λ□ programs. A compiler of sorts.
Me: <Closes laptop lid>
I am sure that theres something useful happening here, but it is definitely too galaxy-brain for this guy.
Me: Go on I am listening...
> The backend I’m writing is just a program — written in Haskell — that takes as input the internal representation of Agda programs, and outputs λ□ programs. A compiler of sorts.
Me: <Closes laptop lid>
I am sure that theres something useful happening here, but it is definitely too galaxy-brain for this guy.