/dpt/ - Daily Programming Thread

Old thread: What are you working on, Jow Forums?

Attached: 1559892147574.jpg (1280x720, 286K)

Other urls found in this thread:

projecteuler.net/
pastebin.com/raw/7Te6hy9M
dl.acm.org/citation.cfm?id=360216
joelonsoftware.com/2005/12/29/the-perils-of-javaschools-2/
microsoft.com/en-us/research/wp-content/uploads/1992/04/spineless-tagless-gmachine.pdf
twitter.com/SFWRedditVideos

akari-chan on the front page!

Attached: 1550988462339.gif (500x200, 995K)

projecteuler.net/

How's your game coming along?

Attached: ll.webm (914x742, 2.15M)

Qt is the best framework for C++, for doing literally anything.

Attached: 1557147306953.gif (500x491, 376K)

>eyes are getting worse and worse
>no way to fix or improve vision, not even glasses
>programming physically hurts because I'm hunching over and straining my neck just to read text on the screen
I think it's over for me. Time to redo my entire life and hobbies I guess.

Attached: 96ab6fcf7b2a6211f8ec6d0e280c7bb8.jpg (800x562, 52K)

>tfw my boss just complimented me for fixing a huge bug that was preventing us from shipping the product
>mfw it was actually caused by my shitty code and nobody noticed

Attached: 1543739292679.jpg (250x250, 19K)

Currently working on an inventory control system for my department. Writing it in python, using tkinter for the GUI

why dont glasses work?

GTKTARDS BTFO

>nobody noticed
they noticed, they just didn't want to embarrass you

dumb frogposter

why do you suck so bad at your game

Just become a qt grill and be someone's sex slave. Bonus: always enough money and you can stroke your dick all day without worries.

take your meds

Use Forth.

no, that's boring

Don't use Forth.

Game developers are always bad at their own games. Come on, it is natural law.

Girls are bad at videogames

They should be the best at their game, what kind of dev doesn't play their own game

My eyes aren't poor, they're fundamentally incorrect. I'll be going for a new pair next week but I literally already got some new ones a few months ago and saw minimal improvement. If they don't do enough this time then I might just kill myself.

I'm a manly, tall lad with broad shoulders and a tight waist.

post tits or feminine penis

Well, I'm trying to get rid of overhead, so a fuckton of libs wouldn't make sense now, would it?
No repo so far. It's been, what, half a decade since I last worked with CL and I need to refresh my emacs knowledge.

>or feminine penis
He said girl, not boy.

They would never resist the opportunity to make fun of me

>tight waist
Stop it user, I can only get so hard

this gave me an idea for what to code- i am indebted to you

A core dependent type theory for proof carrying code. The main goal is to be simple, making the type checker simple, making the trusted base smaller. Specifically, I'm attempting to polarize dependent type theory so that it admits proof search. Then proofs simply become oracles, streams of bits which the type checker uses to resolve non-deterministic search choices. This significantly compresses the size of proofs, which traditionally end up being far larger than the corresponding executable.

My key observation was that since polarity forces you to acknowledge that computation occurs in a monad, in order to do type level computation you need type level bind, also known as explicit substitution. I actually previously saw a paper about sequent calculus for pure type systems needing explicit substitution, but I didn't grok why until I discovered it for myself. Anyways, I was having trouble with type level computation and compiling pattern matching to eliminators, but it seems to make sense now when I don't ignore the monad.

Attached: 1559905298100.png (620x878, 494K)

This is just the Godot engine tutorial? Are you trying to pretend it's your game?

>Hey Tim, i think Bob has had enough with mockery
>don't make fun of him this time

Okay, dude, this post? It's seriously messed up

What important lesson(s) does Forth have?

lobotomize yourself

Fuck off

TL;DR

None of that shit will ever be useful though.

Good engineering practices > good theoretical foundations.

T-3 days to get robot walking
Config for four legs works. Now I only should throw coordinates at it and it should walk.

Attached: nice.jpg (1366x768, 99K)

Do you know what proof carrying code is?

what is it running on? raspberry pi?

wheres the proof that you're doing anything useful

why should I?

stop with the theory and show me something done

good thread

Attached: 1542506699253.png (550x530, 287K)

>what is it running on?
lots of math

Useless academic wank.

seething brainlet

pastebin.com/raw/7Te6hy9M

Wow, some people woke up on the wrong side of the bed this morning.

but what hardware

I literally only read your post because your anime girl is not a loli

this plus x86_64 right now + pololu maestro pwm controller.
It will run on a raspberry soon, I think. x86 for easier development.

Attached: cool.jpg (3000x2000, 665K)

This is me!

are you the Scottish guy?

ohFuckMe Why is front-end development so bloated?

Attached: roadmap.png (1542x2949, 580K)

So glad to have left that code monkey profession.

no, i am from nazideutschland

the complexity of a programming environment has much more to do with the amount of people using it than it does with the actual problem that needs to be solved

why is this better than metaprogramming in theorem provers?
i'd think that you can just implement different kinds of proof search (and CAS fuckery and such) in meta programs.

um sweaty can you not?

PS: which scottish guy?

there's a guy from scotland in /bst/ that works with drones and the picture looked like it was him

The point is that the untrusted and arbitrarily complex theorem prover should emit a proof certificate that can be easily transmitted and checked by a simple, trusted kernel. "Proof search" in this case is just eagerly applying certain rules and then reading log(N) bits from the oracle (proof) when there's a choice of N rules to apply. See dl.acm.org/citation.cfm?id=360216 for the idea.

not him but I'm planning to build a 3d printed drone with a raspberry pi brain. In the programmnig side I plan to make it fly autonomously

>with a raspberry pi brain
I have no idea about drones, but my mind says that they depend super heavy on good timings. Since linux can't do RT by default you would have to patch RT_PREEMPT, but I am not sure how good RT_PREEMPT really is. Do drones need realtime?

the flight controller should be updated as fast as possible i.e. thruster force to keep stabilization. As that is not computation heavy, a raspberry pi will do

I wonder if you know about model checking? I've heard it's somehow related to theory proofing, programming verification or else. what's the difference?

Model checking is basically a rigorous form of exhaustive testing. In theory, a model checker could be used to produce such certificates for safety and liveness properties.

i'm retarded trying to use python math.tan. i want the angle and i know the opposite and adjacent. shouldnt my calculation be
angle = math.tan(opposite/adjacent)
i'm inputting 2/15 and its outputting 0.0

well it's 0,00232710987008701787228319707878
you're losing precision somewhere

int/int=int

What's the best way to serialize key value pairs where both are strings?
obviously the number of pairs and the key/value sizes have to be serialized before the actual data so that memory allocation can be done easier
but should they be separate or interleaved

well the angle should be about 7, i think the function should be able to handle that before going crazy because the value being too small

i did 2.0/15.0 and it works now. thanks!

what language?

Malboge?

2./15. works too

>The point is that the untrusted and arbitrarily complex theorem prover should emit a proof certificate that can be easily transmitted and checked by a simple, trusted kernel.
do we really need this if there are theorem provers like lean with a small trusted kernel?
does the benefit of this only affect larger theorem provers and finding common ground as to when a proof is correct?.

that really doesn't matter, but sepples

Serious question now, please enlighten me.

Many "big names" in computer science and technology have made comments regarding how good lisp is, ranging from mild (you can't be good programmer if you don't at least known Lisp) to extreme (all languages are inferior to Lisp and are only used for people too dumb to use Lisp). In general, I hear mostly praise.

I am now deciding to learn Lisp, except I don't really want to learn Lisp or Scheme. There are newer and more popular/widely used languages out there, and I think I can kill two birds with one stone (learn FN + pick up a useful language).

I am thinking of the likes of Clojure, Haskell, Erlang, and even Scala. My question is how can I tell which of these will give me the "Lisp experience"? I mean some people call Python and Ruby functional, yet something tells me knowing Python is not the same as knowing Lisp.

I don't understand the question just dump them

>that really doesn't matter,
retard

Lisp is not synonymous with functional. In fact most Lisps are multiparadigm. Common Lisp doesn't even do functional that well.
Clojure is the only one of these which is a lisp. Purists don't consider it a Lisp, but it's splitting hairs. Haskell and Erlang are valuable in their own right but they're not Lisp.

Clojure if you absolutely need something "modern".
Otherwise pick Common Lisp (SBCL is a good implementation, but there's more than one good one) or Racket or another Scheme like Chicken Scheme.

Any good IRC channels and/or servers for general programming discussion?

If popular = useful, don't learn Lisp.

this kind of lisp-praise is a cult.
learning lisp will provide you with some value, but not knowing lisp is nowhere near as bad as those comments make it out to be.

it really doesn't
optimal serialization methods for types that are contiguous blocks of memory are going to be the same regardless of language
memory allocation is never cheap

user, the angle is computed using arctan, not tan.
tangent = opposite/adjacent;
angel = math.arctan(tangent);

Okay so when people refer to the elegance or essence of Lisp (the stuff which makes it so great) what are they referring to? It would be good to have some criteria to judge other languages by. Like why is Clojure not Lisp and does it even matter?

Could you tell me a little why Clojure but not Haskell, for instance?

Don't ever listen to anything "big names" in computer science say if those big names include people like RMS

I think that those comments don't really refer to Lisp specifically. It's more of a knee jerk reaction against languages like Java. See joelonsoftware.com/2005/12/29/the-perils-of-javaschools-2/ for example.

>useful language
>haskell
pottery

if you want modern+functional+lisp racket is the best.

oh I see you are a PLT researcher
what could be a good roadmap into higher order model checking/program verification?
how about this: steshaw.org/plt/

If there isnt a specific problem then there is no "best" way between interleaved vs not. Is it being transmitted over a very slow wire and you need values before you can send them off elsewhere? Then interleave it. Serialize the number of pairs and allocate mem up front. I don't understand your dilemma.

He's not asking about what .toString() method to use, he's trying to do a microoptimisation.

>PLT researcher
where do these idiots come from?

finally got around to read this:
microsoft.com/en-us/research/wp-content/uploads/1992/04/spineless-tagless-gmachine.pdf
much more readable than I thought, might make for a good project to implement the mechanisms described there

Lisp users would generally say that what separates Lisp from other languages is the use of s-expressions for both code and data. This makes it easy to implement powerful macro systems, for example.
Clojure is the only language mentioned which uses s-expressions. It's different from other Lisps in that it changes a number of the other primitives but I'd say the heart of Lisp is still there.
Haskell is a whole different thing. That's pure lazy functional programming with a rich static type system. Haskell is a specific set of tools that forces you to write programs in a particular way. Lisp gives you the ability to fashion any tools you like and program in whatever way you want. Both valuable but distinct approaches.

Lean works in much the same way (most proof assistants do), but AFAIK it is not designed to have particularly compact proof certificates.

>If there isnt a specific problem then there is no "best" way between interleaved vs not.
i figured it'd be something like that
that'd probably be why i'm having trouble being decisive
>I don't understand your dilemma.
programming while very tired

Guys I think I'm retarded
If I send 1024 bytes every 1 millisecond, does that equal 7.8125 Mbit/s ?

Attached: 1512219834979.jpg (374x347, 39K)

Learning Lisp right now, buddy.

For me, it's lots of fun. The community's small, but it's very enjoyable to code and the interactivity of it makes for a unique experience.

As will all languages, you'll only fully leverage a language's capabilities if you enjoy it. So, give it a try. If nothing else, it'll yield transferrable knowledge and a different point of view.