λ - programming

>>11323
Lean is cool. Its syntax is very similar to Coq's and it's even built on the same logic.

>For reverse engineering for example, it would be great to prove that the reconstructed source code does the same as the original
I'm not sure this would be the right job for manual verification. You tend to run into a lot of repetitive and tedious proofs when proving these things from the bottom up. It's a different matter when you already have high-level models of both sides and want to prove specific equivalences.

What you want is to prove functional correspondence of two programs. Depending on the level of abstraction, what you want is something like symbolic execution or model checking, which is a mostly automated (depending on how you obtain your model) method for proving correctness of programs. There are many tools for this, too.

One of them is SAW (http://saw.galois.com/index.html), which uses SMT and symbolic execution to verify properties of C and Java programs. The guys from Galois, Inc. had a talk recently about verification of cryptographic functions using SMT; the slides are on GitHub, for those interested: https://github.com/GaloisInc/sat2015-crypto

>I can imagine jobs in that area to be very well paid.
I can confirm. They're also not the easiest and you must know tons of theory to be efficient and innovative, though.

>>11344
Here's another one: http://ilyasergey.net/pnp/
I have tons of links to other resources, but I'd be too embarrassed to publicize them in their current form.

>>11345
BTW, I was considering writing a short article (perhaps even series) about some topic from this area, but I'm not sure how useful it would be given the amount of good resources that have already been written.

>>11346
That would be really cool. Maybe you could get it into the lainzine?

>>11348
Oh of course, I meant to write "a short article for the zine", but it got lost somewhere between editing.

>>11345
Considering that reconstructing C source is already tedious and has to done function by function (even with help of a decompiler) adding proofs seems like a linear overhead.
I don't know the exact distinction between all these terms (model checking, etc.) but I think you can always convert there to a proof later.

I imagine that one could develop tools to automate this work: Mark a few correspondences in source code and binary flow graph, or source variables and registers, and let some algorithm figure out the rest.

>One of them is SAW (http://saw.galois.com/index.html), which uses SMT and symbolic execution to verify properties of C and Java programs.
I wonder how well it copes with memory accesses (cryptographic function are mostly pure).

>>11091
I would think a phone number makes more sense as a series of 4-bit values, so as to emulate any sequence of DTMF signals.

>>11199
It's better to do the research early and plan for all the edge cases rather than have to add support later.

Seriously, just store the phone number as a string. You can do a basic regex to ensure only valid chars are allowed (numbers obviously, and also allow users to do stuff like enter + symbols for country codes), and worse case if your application has to pass the numbers to a dialer you can just iterate over the character array and check to make sure you only 'dial' numbers. It really doesn't cost that much computationally and saves a lot of other hassles.

This all comes back to the "don't prematurely optimise" principle.

>>11091
>calculating over data structures
Actually a very important and increasingly neglected idea, certainly not one helped by languages that emphasize data structures like Java (or Python etc). I recently came up with an algorithm for finding certain musical scales that uses numbers to represent scales (their binary representation reflects the notes contained in the scale, with the least significant bit representing the 1st note). It found millions of scales rather than thousands, and the critical parts were ~20 lines of code instead of close to 150! The math involved was elegant and clear. Over-engineering can be a serious problem.

I've found Forth to be a rather inaccessible language unfortunately. Someday I want to learn it properly and try a large project with it, but I'm not nearly capable right now. Using memory allocation in Forth is confusing to me. Maybe I'll try to rework the music scales code to work in Forth, just to see how it goes; I don't think I'd need to use conditionals or data structures given all that I've learned.

>>11231
>I've found Forth to be a rather inaccessible language unfortunately.
>Using memory allocation in Forth is confusing to me.
While there is an optional memory allocation word set that provides allocate, free, and resize in the same vein as malloc, free, and realloc (gforth even implements them directly with the C functions) you really shouldn't need them in many cases. Most memory management in Forth should adhere to the stack model.
You should obviously use the data stack for most things and you can even use the return stack, as long as you don't need the values below it, meaning you can use the return stack and call other words without issue. You just need to pop your value from the return stack before you need to return from the word that placed it there.
As for allocating arrays, you should generally use allot when creating a word to associate the space with it. Allot, ,, and c, all use here to determine where the next data space address starts and reserve contiguous space from there.
Here's one way to define an array:

create array 20 allot

Here's one way to create a defining word that defines arrays:

: array ( n "name<space>" -- )  create allot
  does> ( n -- addr )  + ;

This word doesn't check array bounds, but this would be easy to add by also storing the length of the array in the newly-defined word and adding a check. All DOES> does is define the behavior of the CREATEd word and places the address of the data space of said word on the stack when being executed. This makes it easy to get the indexed address by simply adding.

I know I went on a tangent really, but I don't really have anyone else to talk to about these things. My main point is memory management in Forth is actually really easy. If you're coming from a GC'd language, you just have to understand that a static memory model isn't that hard to deal with and is usually sufficient. You just have to process certain data in chunks instead of all at once.

>>11238
Thanks for the advice.
>If you're coming from a GC'd language, you just have to understand that a static memory model isn't that hard to deal with and is usually sufficient
I think this is my main struggle. I probably overcomplicate problems because I don't understand how to do things with just static memory.

>>>/q/7286
CatChan script can give for you
1. catalog mixture.
2. finder of recent posts.

OK, let me tell how to configure it.
1. setting -> load_default -> I want...24 -> reload
2. setting -> Board Group -> write 'cyb/tech/,lain/tech/,lain/cyb/,8chan/tech/ -> select cyb/tech/
3. You can show site's name if you want.
4. You can save your configuration by clicking 'save'.

You can see U:X/X, this means number of unread replies to you and unread replies (to others, includes to you) respectively. Threads which have unread replies are sorted first by default, so you can read all replies in recent 24 hours. Unread replies are marked red in threads, and you are jumped to the replies automatically when you open threads. The script has other functions, I can tell you about that if you want.

If you have any feedback, please leave it here.
Thank you for reading.

I released an update. Minor bugs are fixed.
https://raw.github.com/Dogman8/CatChan/develop/CatChan.user.js

>>>/tech/12952
CatChan can provide both tagging, internal and external(site-wide now). You can aggregate threads which have a tag from a board by default. If you want to aggregate them from all over the site, click '20VBs ... (for lainchan)' to enable scan.

By internal tagging, you can make subboards like #posix or #GNU, though I think lain/tech/ is not so fast and don't require subboards. Anyway, tagging is useful when you want to filter threads by its topics.
By external tagging, we can evaluate moderators. I think good moderator is a person who have done good moderation, but criteria of such depends on each people, so moderation matters will not disappear. Therefore, I provide another way to solve this. If site provides /tech000/, /tech001/, ... , /tech999/, the script can gather threads by both way, tagging and boards group. If all boards /techXXXX/ have a tag #tech as a board's tag, all their threads will appear in #tech virtual board. Or you can make a boards group like >>10997. This requires user's configuration, but if site provides some configuration template like boards.json, I'll add function to read it. By these, we can choose where we'll create a thread. You can make a thread where the moderator whom you trust lives. This means evaluation of moderators.

>>>/q/7548 or admins,

Now you moved a thread >>>/tech/12952 to >>>/q/7601, this was caused by a limitation which is that a thread must belongs to a board. But you can avoid this in virtual board system. OP placed the thread in /tech/, because OP thought it should be read by people of /tech/, this is right. And you moved it to /q/ because you thought it contains meta discussion, this is also right. But /q/ is a board for meta discussion about site, so ordinary /tech/ people don't come. Therefore thought of /tech/'s mod isn't known by people of /tech/, this is bad. The best solution is that place a thread to both boards /tech/ and /q/. You can achieve this by copying every post if you have such system, or use tag to make virtual boards. In virtual board system, you can add the thread to #q if your post contains #q, it's very simple.

And you can train moderators in virtual board system, this changes lainchan from a private chan to a public chan which we can cooperate with all aspects including moderation, and this is what I misunderstood 8chan was such. Now you are player of moderators, sometimes you delete or give a ban. In virtual board system, you should become coaches or managers of moderators, and you'll hire or fire them. As I described in >>11166, virtual board system contains evaluation system of moderators, so you just choose popular moderators to maintain good atmosphere. This is similar to 4chan's hierarchy, Admin-Mods-Janitors, but the biggest difference is that we citizens can evaluate moderators. On the contrary, only mods or moot friends can evaluate janitors and that is not open for public in 4chan, so the moot made mistakes. 8chan limits cooperation to code or money, but moderation is the biggest and the most difficult matter in chans. If you want this chan to be a public chan, training moderator system is required. CatChan can give it.

I posted my dogma in 8ch. If you want to know, refer this. Pic is that.
http://8ch.net/next/res/1655.html#q1692

>>11228
I'm not overly familiar with this service, but from looking into their FAQ's it seems like it's just breaking files into chunks, encrypting the chunks, uploading some/all chunks to their cloud, and then the client downloads and unencrypts the chunks on it's end. Almost certainly some kind of validation e.g. each encrypted chunk has a checksum listed which the client verifies after dowloading, if they don't match redownload and try again.

The actual core technologies would be pretty simple to implement, since this kind of crypto and reliable download mechanisms have existed for years / decades. Building the various client apps, web services, middleware platforms, etc. around those core technologies would be pretty time consuming though.

If you wanted to build a hacked-up clone of this for small scale e.g. sharing between friends, you could have the following setup:
You, your friend, and a virtual private server all have torrent software installed. The VPS also has a torrent tracker setup.
You and your friend have a shared symmetric key, or you encrypt the files you want to send with their public key. NEVER allow the VPS to have the decryption key.
You create a torrent of the files you want to send them, and also ensure that the torrent exists on the VPS's torrent software and in the tracker.
You send your friend the torrent.
Even if you are offline, they can dowload the files from the VPS which is seeding the torrent. The VPS cannot open the files because they are encrypted, so even if it gets seized the contents are safe.
Then you just email the torrent file to your friend, and they can start downloading.

Wrap that in some scripts to automate the upload to the VPS part and you have most of the functionality taken care of. No web interface, but who really needs it.

There's tons of distributed systems that'd allow for it.
Take a look at GNUNet, morph.is and ipfs.
One thing that has worked well for me and my friends has also been creating a hidden service, forwarding it to a lokal http/ftp/gopher server and sharing your files over that.

Replace:

(loop for i from 1 to 100 do ...)

With:

(loop i 1 100 ...)

>>8596
I was under the impression that this was all casual discussion that wouldn't actually lead to anything being implemented.
>>8611
Reader macros can do that. It should all boil down to lists and atoms at some point though.
>>8612
You have to take into consideration that `for' is not the only possible opening loop clause. The current setup works to make the macro readable as if English while also eliminating ambiguity.

I can't justify just letting this thread die yet.
Let's see if there's any more discussion.

>>10207
Did anyone even do anything? I read through the thread and don't really see much progress. Maybe we need some action instead of just discussion.

>>4023
Bump for existence

>How do you access these sites?
Gopher protocol is really easy, so if you don't have working client you can just telnet into server.
I use lynx.
If you want some real GUI, install overbiteFF (firefox addon) or connect through some proxy.
http://gopherproxy.meulie.net/
>How would one go about making a gopher website?
Read this
http://gopherproxy.meulie.net/gopher.floodgap.com/

Can someone tell me how I would begin to participate in IRC (not just on Lainchan)? I have a client, I know how it all works but I don't understand how communities function on them.

>>11174
> I don't understand how communities function on them
There's two forms I've seen so far.

Social hangouts or circlejerks, like #lainchan. Pretty much the same as hanging out with friends IRL.

Channels centered around a project, like #haskell or #nixos. They'll talk about the development of the project and answer your questions.

>>11175 That makes sense, thanks. Most IRC channels I've gone on before have just been empty with hundreds of idle users, is this normal?

>>11176
Yep, though I have no explanation for this.

>>11180
That's perfectly normal.
Most people have their IRC clients open while doing other stuff or even use bouncers.
You'll usualy get a reply if you start a conversation, though.

>>11015
A good portion of the page count is probably exercises. This is a first year college textbook, so it's made for big classes where the professor just assigns 20~ easy-to-check problems a week.

It's not like the books in the 8chan link which are shorter and have harder, more abstract problems.

>>11016
>>11017
sure I understand all that but it's still a LOT of book to get through.

that 8chan list looks a little shaky at the entry levels but CLRS and Concrete Mathematics are no-brainers.

>>10143
Combinatorics and Set theory can be really fuarrrkin' hard.
Especially if youre not attending classes or youre learning its very structured.
D/w man, you have motivation, all you need is discipline, and you will be good!

Do you need multivariable calculus before linear algebra?

>>11184
you should be learning linear algebra before multivariable calc.

>>9900
This. Fortran got it all figured out from the beginning.

I've been interested in learning Lua for quite a while now.
What's the best/easiest resource for this? I'm much better with interactive stuff than I am with just reading.

>>10949

That's the magic of C anon, if two languages have a C FFI you can always get them to interoperate.

I've gotten Haskell and Guile Scheme to interoperate in the same fashion.

>>11011
Bump

>>11011
I've been learning how to use Lua by making a module for it using the Programming in Lua 3rd edition which uses Lua5.2

>>11111
missing )) at end.
dat get tho

>>11111

print("Greetings, "+input("What is your name?"))

48.

Ruby:
puts "What is your name?"
name=gets.chomp
puts "Greetings, " + name.to_s

70 chars

>>11148
Nice. I assume that this works because the class of the object returned by input() is str, so the two strs can be concatenated directly, without the need to wrap input() in format()?