Daily Programming Thread

Old /dpt/ at What are you working on?

Other urls found in this thread:

archive.rebeccablacktech.com/g/thread/S57357273
twitter.com/NSFWRedditVideo

How much do you hate yourself OP?

var blockQuotes = document.getElementsByTagName('blockquote');
var blockQuotesArray = Array.from(blockQuotes);

var words = (function() {
var _wordArray = [];

function add(words) {
_wordArray = _wordArray.concat(words.split(' '));
}

function get() {
return _wordArray;
}

return {
add: add,
get: get
}
})();

blockQuotesArray.forEach(function(elem, index) {
words.add(elem.innerText);
});

console.log(words.get());


Ok, lads. I've done my bit. You need to add to it now.

The acronym in the title helps people with sane auto-watch filters.

kthx

>i hate anime, where should i go?
>oh i know, Sup Forums

t. op

>The compiler for that platform, written within the language, provides the assumptions
How?

Bigotry is a reason for WHY america sucks. Don't perpetuate the problem, op.

What do you mean how?

I don't get how you're not getting this

the virtual machine and shit
the compiler
etc

then you get back machine code

But how do you get a proof that addition of machine integers is commutative?

the compiler for that platform provides it
or effectively the virtual machine description asserts it
and if it has an emulator then it's proven to work for the emulator

>the compiler for that platform provides it
Is it proven or assumed?

yes

it's a description of the machine

That wasn't a yes or no question.

america sucks because of people like you using the word "bigotry" for everything

America sucks because of you

ffs
it is a description of the machine
how can you be this misunderstanding

x = 2
is x 2? is that proven or assumed?!

That would be an axiom, not a proof.

char string1[1024];
char string2[1024];
printf("Foo\n");
freopen("/dev/null", "a", stdout);
setbuf(stdout, string1);
printf("Bar\n");
freopen("/dev/null", "a", stdout);
setbuf(stdout, string2);

Is string2 "Bar\n" or "Foo\nBar\n"?

What programming language should I learn? or know well?

>That would be an axiom
Is that reply proven or assumed?

>it is a description of the machine
But how do you know it's correct? You either have to prove it, test it or assume it. And in the latter two cases there is some trust involved.

Since you seem to be eager to "correct" me on how dependent types work I'm surprised you don't seem to understand the concept of proof.

Python

and since when can proofs not use axioms?

>But how do you know it's correct?
IT GIVES YOU FUCKING BINARY MACHINE CODE FOR FUCKS SAKE
THAT'S JUST A GLORIFIED INTEGER
THEY COULD USE THAT OUTPUT AS A FUCKING PHONE NUMBER AND CALL IT FOR ALL YOU KNOW

What's the machine code for commutativity of machine integer addition?

>
[smug-anime-girl.webp]

Spoken like a true bigot.

Teach me LINQ /dpt/

>b-but how do I know the description matches the machine

I fucking hate you
Fuck you
You dumbass


You know it works on MACHINES THAT FIT THE FUCKING DESCRIPTION

What the fuck is next?
Are you gonna ask me how it knows that the variable names are correct too?
How it fucking knows that some idiot is not gonna take the machine code, print it off and eat it? Someone like you?

var blockQuotes = document.getElementsByTagName('blockquote');
var blockQuotesArray = Array.from(blockQuotes);

var words = (function() {
var _wordArray = [];
var _wordObj = {}

function add(words) {
_wordArray = _wordArray.concat(words.split(' '));
}

function log() {
var word;
var count;

while(_wordArray.length !== 0) {
word = _wordArray[0];
count = _wordArray.reduce(function(n, val) {
return n + (val === word);
}, 0);
_wordArray = _wordArray.filter(function(elem) {
return elem !== word;
});
console.log(word + ': ' + count);
}
}

return {
add: add,
log: log
}
})();

blockQuotesArray.forEach(function(elem, index) {
words.add(elem.innerText);
});

words.log();


Getting somewhere, but it's a bit unaesthetic, sorry.

or since you probably still won't understand

>HOW DO I REMOVE ALL THE AXIOMS FROM THIS PROOF?

But what the proof it fit the description though?

I'm fucking done

>You know it works on MACHINES THAT FIT THE FUCKING DESCRIPTION
How? How do you know the machine fits the specification?

You getting angry is not going to make me stop replying to you.

All I'm saying is that any axioms made by the programmer (typically in FFI) should be visible and explicit.

>How do you know the machine fits the specification?
FOR FUCKS SAKES

>archive.rebeccablacktech.com/g/thread/S57357273
wtf. Seems like a normal post. Thought it was nsfw 2bh

ok, here is the super retardo dumbass example

what the fuck stops someone from taking that machine code output and eating it?
their stomach doesn't assert the commutativity of integer addition

>food analogies

>food analogy
what the fuck are you talking about?
i'm saying what stops someone literally eating the output

where was your proof then?

Maybe OP deleted it because he was embarrassed he posted a thumbnail.

you basically want your language to be God and know everything since it can apparently prove arbitrary statements about the real world

I get eat now

What?

No?

Hello Pajeet, are you lost?

Also, that's what YOU said.
>the compiler for that platform provides it

yes

your language can determine whether or not a machine fits an abstract specification, remember?

so why can't it do other things like determine whether or not a particular tree has fallen over

When did I say that?

>Also, that's what YOU said.
>>the compiler for that platform provides it
No you muppet
The compiler provides abstract descriptions of the platforms for which it compiles
The platforms for which it compiles ARE those abstract descriptions
whether or not they correspond to the real world isn't something the language can fucking know, any more than it can know whether or not they correspond to platforms that might be made a million years in the future

>whether or not they correspond to the real world isn't something the language can fucking know
Yes.

and as an example, the machine code produced by said compiler might be put on a completely different fucking machine that it wasn't compiled for

what then?

your language isn't God

By "yes" I mean I agree.

Doing some regex on this chunk of text
aria-describedby="description-id-970548" dir="ltr">Friendly Baby Fox!)(.*)(?:)

It doesn't stop properly at , and will continue waaaay down to a second including awhole bunch of shit I don't want.
If I change it slightly to
(?:"description-id-[0-9]*" dir="ltr">)(.*)(?:

ok

so whats the problem

you know your code fits that abstract description, and it can be a requirement in many different ways

There was never a problem.

nevermind, i needed a lazy operator on the capture group

then what were you complaining about?

I was never complaining.

whatever

at least you're over your silly idea of building something completely redundant into the language

Which was?

stupid, it was stupid

axioms are already handled perfectly well by function types

Are you saying that e.g. the main function should have parameters for the axioms it postulates, and pass the arguments around everywhere as proofs?

All I was saying was to have a feature like Agda's postulates but, upon building the project, the axioms are identified so they can be tested or simply trusted.

>tfw ncurses uses more memory that the base program
All that element packing for nothing

>premature optimization

why would that be in the main?

the compiler for that language and all are inside the language
the output is just machine code

you know that the machine code describes a program you envisioned for a particular abstract machine

That's completely fucking irrelevant.

literally the same thing. may be different if you said coders/programmers from computer scientists

Why is this wrong? We're using MASM

you don't even need main

Literally the same thing. Maybe different if you said corders/programmers/computer scientists from mathematicians

Then how do you propose to introduce axioms with function types only?

>writing in c
>using libraries

You mixed up low/high.

a coder and a programmer is the same thing because the words mean the same thing, i.e. a person who writes code. a computer scientist is someone who works with the theory of computer science, which is as distinct from programming as geometry is from using a protractor

what the fuck are you even trying to say?

you have an abstract description and dependency and abstract code in a million fucking different possible ways, one method of dependency being a function type

what is the damn problem

you got your results out, which could be done in any of a variety of ways

you take the machine code and you put it in a file or some shit, or maybe your IDE does it automatically

Not c faggot

There's no fucking problem. You're the one saying I'm wrong without actually articulating why, and providing a non-alternative.

I see how he switched them, but I don't get how is mine wrong if I said explicitly where I'm storing each character

it switches like this
abcd
acbd
bcad
bcda

Just started to lean programming at school. It's all in Java.

>I can read it and understand it decently
>Tfw struggle to finish labs and create my own program.

Function types can give you dependency
Alternatively you can be working from an abstract description
How you don't understand that I don't get

What abstract description?

Originally I was talking about postulates (well I used the word assumptions) and you said they were unnecessary because of dependent function types.

>As we learned above, poor performances in technical interviewing happen to most people, even people who are generally very strong. However, when we looked at our data, we discovered that after a poor performance, women are 7 times more likely to stop practicing than men

read sicp

which language?

women are fragile, they shouldn't be asked technical questions because it excludes women from jobs in tech

yeah, sure

sub isodd($) {
my $odd = 0;
for my $i (1 .. shift) {
$odd = !$odd;
}
return $odd;
}

sub odd($) {
my $n = shift;
return 1 if $n == 0;
return &even($n-1);
}

sub even($) {
my $n = shift;
return 0 if $n == 0;
return odd $n-1;
}

I assuming you mean structure and interpretation of computer programs.

>language has no decent tui library
why even live

I'm trying to write a program that gives out two random numbers to multiply and the user has to guess the right answer. Once the right answer is given, a new set of two numbers are given until the user force quits. I can't seem to get a new set of new numbers and the same two numbers repeat.

srand((unsigned)time(0));
while (true) {
cout

Ada/C

like a datatype that expresses programs on that platform

e.g.
data thing : Type where
one : thing
add : thing -> thing -> thing
com : (x:thing) -> (y:thing) -> (add x y = add y x)


in this case i cant remember what = things are called but the point is it asserts the equality of those two things

alternatively you could have a function in the library you're using

commute :: (x:a) -> (y:a) -> (x + y) -> (y + x)

any number of different ways

rand it again papi
with gettimeoftheday()

whoops, just (x + y) -> (y + x)
or
commute :: (x + y) = (y + x)

That is all well and good but you're missing the point of all this which is proving vs. postulating that the machine integers are commutative under addition in the first place.

It just sounds like you heard something about proofs and thought you would spout all your dependent type knowledge at me to seem smart.

>That is all well and good but you're missing the point of all this which is proving vs. postulating that the machine integers are commutative under addition in the first place.
Not having this fucking conversation again
either the "real thing" meets the description or fucking not
either way, your language can't fucking know that, or what it's run on
all you know is that it works on things that meet the specification
jesus christ

what language? C#?

what are the freatures of ada?

cuteness

Safety

>either the "real thing" meets the description or fucking not
>either way, your language can't fucking know that, or what it's run on
>all you know is that it works on things that meet the specification
And I'm talking about the process of determining whether the specification is met.

>safety
hahahhaha
might as well use rust and a type system

Not a part of the language