gopiandcode

9 ms·

31.
LLMs pose an interesting problem for DSL designers(kirancodes.me)
220 points by gopiandcode 1y ago|151 comments
32.
The looming problem of slow and brittle proofs in SMT verification(kirancodes.me)
4 points by gopiandcode 1y ago|0 comments
33.
by gopiandcode 1y ago
Ahh, that is a valid point; so it's not quite as clear as using something like quick check, but it does feel like there is increasing interest and activity in people trying out doing exploratory maths in Lean itself. I mention it in th
34.
by gopiandcode 1y ago
Fwiw there's also an Emacs plugin which is what I use and it works really well. For using Lean as a theorem prover, this book is pretty good: https://github.com/lean-forward/logical_verification_2024 Also, Lean is
35.
by gopiandcode 1y ago
Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd
36.
How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean(kirancodes.me)
81 points by gopiandcode 1y ago|17 comments
37.
by gopiandcode 1y ago
I am more than aware of Typescript, you seem to have misunderstood my point: I was not describing a particular type system (of which there have been many of this ilk) but rather conjecturing that targeting interfaces specifically might make
38.
by gopiandcode 1y ago
The visualisation of how the model sees nullability was fascinating. I'm curious if this probing of nullability could be composed with other LLM/ML-based python-typing tools to improve their accuracy. Maybe even focusing on interf
39.
Functional vs. Data-Driven Development: A Case-Study in Clojure and OCaml(kirancodes.me)
6 points by gopiandcode 2y ago|1 comments
40.
by gopiandcode 2y ago
I find this particular choice of syntax somewhat amusing because the pipe notation based query construction was something I ended up using a year ago when making an SQL library in OCaml: https://github.com/kiranandcode/
41.
LeanSSR: An SSReflect-Like Tactic Language for Lean(github.com)
2 points by gopiandcode 3y ago|0 comments
42.
by gopiandcode 3y ago
Please also consider how much less inclusive and accessible computing would be if access to development tooling was placed behind such exorbitantly priced paywalls... The things we have at the moment aren't perfect, but I feel like the
43.
Sisyphus – Mostly Automated Proof Repair for Verified Libraries(verse-lab.github.io)
2 points by gopiandcode 3y ago|0 comments
44.
Rhombus in the Rough: A 2D RPG implemented in the Rhombus Racket Lisp dialect(github.com)
2 points by gopiandcode 3y ago|0 comments
45.
Petrol: Embedding a type-safe SQL API in OCaml using GADTs(gopiandcode.uk)
3 points by gopiandcode 3y ago|0 comments
46.
I Wrote an Activitypub Server in OCaml: Lessons Learnt, Weekends Lost(gopiandcode.uk)
154 points by gopiandcode 3y ago|108 comments
47.
by gopiandcode 4y ago
To be fair, the distinction here is about actions by a government, versus actions by private entities. Opposition to the government banning a website does not necessarily mean that you would oppose private companies refusing to provide serv
48.
LLaMA-based Emacs Search plugin(old.reddit.com)
2 points by gopiandcode 4y ago|0 comments
49.
by gopiandcode 4y ago
> If not, how do you reconcile this belief with the right of scientists and publishers to sell their productive labor? As many others in the thread have said - the profits from the paper paywalls go to the publishers, reviewing is done b
50.
Show HN: A web front end for your Org-files(codeberg.org)
92 points by gopiandcode 4y ago|13 comments
51.
by gopiandcode 4y ago
Funny you should mention that - I actually ran into another in-proportion solar system park model in Eugene, Oregon, USA: https://eugenesciencecenter.org/exhibits/eugene-solar-system...
52.
by gopiandcode 4y ago
Wow! GPL-licensed, Free as in Freedom, encrypted note taking! This is great. I think I'll probably end up self hosting this just on principle, but I signed up for a year just to show support! The fact that the Notesnook community is on
53.
by gopiandcode 4y ago
> I see this misunderstanding constantly online - honestly it's hideous to see people twisting Popper's pro-free-speech message into an excuse to crush those they misunderstand or disagree with. Literally inverting his meaning.
54.
by gopiandcode 4y ago
Yes, good catch! I actually wrote the fold predicate thinking of fold left, hence the naming, but as the same predicate can simulate both fold left and right, for the purposes of the blog post, I figured I could get away without renaming th
55.
by gopiandcode 4y ago
> It's not clear whether the author means to say foldl and foldr are equivalent, or only that any foldl call which terminates can be converted into a foldr call. Oh, no, I wasn't trying to say that they were equivalent in gener
56.
Unifying fold left and fold right in Prolog(gopiandcode.uk)
90 points by gopiandcode 4y ago|15 comments
57.
Racket-Rhombus: To Sexp or Not to Sexp?(gopiandcode.uk)
2 points by gopiandcode 4y ago|0 comments
58.
by gopiandcode 4y ago
Shameless plug, I also maintain an OCaml implementation of egraphs (named ego) at https://github.com/verse-lab/ego While the most popular implementation at the moment seems to be egg in Rust, I find that OCaml serves a
59.
by gopiandcode 4y ago
> > Copyright and licensing are bad, actually. > This is why we have "Copyleft". This. Exactly. It's suprising how many developers have strong anti-copyleft/anti-GPL opinions while being completely uninformed on
60.
by gopiandcode 4y ago
I feel like you're missing the forest for the trees here - making code freely shareable and remixable is exactly the purpose of GPL and other free-software licenses, but you can bet that the proprietary codebases Copilot will be used i

More ›