ชีวิตป.เอกเทอมสาม

Posted on March 30, 2015

2


อัพเดทข่าวคราวสำหรับครอบครัวและเพื่อนที่อยากรู้ความเป็นไป
สำหรับความเป็นไปของเทอม 2 ให้เข้าไปอ่านที่นี่
(https://amchiclet.wordpress.com/2014/08/20/%E0%B8%8A%E0%B8%B5%E0%B8%A7%E0%B8%B4%E0%B8%95%E0%B8%9B-%E0%B9%80%E0%B8%AD%E0%B8%81%E0%B9%80%E0%B8%97%E0%B8%AD%E0%B8%A1%E0%B8%AA%E0%B8%AD%E0%B8%87/)

อันนี้เขียนย้อนหลัง เกี่ยวกับหน้าร้อนปีที่แล้ว (พฤษภาคมปีที่แล้ว)

ถือว่าเป็นซัมเมอร์แรกตั้งแต่มาอยู่ที่นี่

หลังจากได้เดวิดเป็นอาจารย์ที่ปรึกษา
เดวิดขอร้องให้เราใช้หน้าร้อนนี้ทำวัจัยที่มหาลัย

ก็จ๋อยๆไปนิดเพราะอดสมัครฝึกงานแถวๆ ซิลิคอน ว่าเล่ย์ ที่เค้าล่ำลือกัน
แต่โดยสรุปแล้วมีเรื่องสนุกๆเกิดขึ้นเยอะเหมือนกัน


การเรียน


เทอมนี้ไม่มีเรียนเฟ่ย


การวิจัย


เดวิดอธิบายโปรเจควิจัยให้เราฟัง

เราก็พอได้ไอเดีย แต่ยังเลือนลางอยู่

เดวิดก็เลยเริ่มจัด textbook มาให้หนึ่งเล่ม หนาประมาณ 600 หน้าถ้าจำไม่ผิด
แล้วเดวิดก็บอกกับเราว่า “อ่านทั้งเล่มเถอะนะคนดี”

ก็เป็นหนังสือเกี่ยวกับว่าพวก compiler มันทำอะไรกับ code ของเราให้เร็วขึ้นบ้าง
เพราะว่าโปรเจคของเราจะต้องเอาไปใช้

จากนั้นไม่นานเดวิดก็มอบหมายภารกิจอีกหนึ่งชิ้นให้ ก็คือ
ให้ไปเยี่ยม อาจารย์อีกคนนึงซึ่งชื่อว่า เจเรมี่
แล้วไปเรียนรู้กับเค้าหนึ่งสัปดาห์ว่าโปรเจคต้องทำอะไรบ้าง

ก็จัดไป

บินไปลงที่เมืองที่ชื่อว่า philadelphia (อ่านว่า ฟิน ลา เดว เฟีย)
ซึ่งเป็นเมืองที่คนชอบเยอะมาก ยกเว้นเรา เพราะรู้สึกว่าเมืองมันน่ากลัวๆยังไงก็ไม่รู้

ไปถึงแล้วก็นั่งรถไฟไปหา เจเรมี่ ที่มหาลัยของเค้า

พอเจอเจเรมี่ เค้าก็พาเราเข้าไปในออฟฟิส

เจเรมี่ก็ให้คำสั่งแรกคือ จงโหลดโปรแกรมที่ชื่อว่า isabelle (อ่านว่า อิ ซา เบว) แล้วเปิดมันขึ้นมา
ระหว่างโหลดอยู่ เจเรมี่ ก็ส่ง pdf ไฟล์มาอันนึง
แล้วบอกว่า จากนี้ไปเราจะอ้างอิงหนังสือนี้เป็นจุดเริ่มต้นของงานวิจัยเรา

ทุกๆอย่างก็เริ่มเป็นชิ้นเป็นอัน

สรุปว่าโปรเจคของเราก็คือ การหาวิธีทำให้ compiler พันธุ์ดุ ผลิต code ที่เร็วขึ้น

ขยายความ compiler พันธุ์ดุ

ปกติ compiler ดีๆปัจจุบัน มันทำหน้าที่หลักๆก็คือ
1. หา bug ใน code เท่าที่หาได้
2. ทำให้ code เร็วขึ้น
3. แปลง code จากภาษาที่มนุษย์เข้าใจ ให้เป็นภาษาที่เคร่ื่องคอมพิวเตอร์เข้าใจ

ทีนี้ตัว compiler เองมันก็มี bug เหมือนกัน
แล้วในกรณีที่แย่ที่สุดคือ compiler แปลง code ผิด

ผลลัพธ์คือ code ที่ผลิตออกมา อาจจะมีช่องโหว่ ให้พวก hacker จู่โจมได้
เช่น เครื่องบินสำรวจอาจจะโดนข้าศึก hack แล้วยึดไปได้
(เอาลิงค์ไปดูมันส์ๆ http://www.cbsnews.com/videos/creating-drones-that-cant-be-hacked/)

มันก็เลยมีการวิจัยเกี่ยวกับ compiler พันธุ์ดุออกมา (ชื่อวิชาการว่า verified compiler)
ซึ่งเป็น compiler ซึ่งได้พิสูจน์ทางคณิตศาสตร์แล้วว่า ไม่ได้เพิ่มอะไรผิดๆเข้าไปใน code

แล้วการพิสูจน์ทางคณิตศาสตร์เนี่ย
ถ้าเขียนบนกระดาษ มันอาจจะพิสูจน์ถูก พิสูจน์ผิดได้
คนเราก็มักจะทำความผิดพลาดเสมอใช่มะ
ก็เลยมีโปรแกรมสำหรับให้คอมพิวเตอร์ช่วยตรวจข้อพิสูจน์เหล่านั้น
ซึ่งหนึ่งตัวอย่างของ โปรแกรมช่วยเขียนและตรวจข้อพิสูจน์ก็คือ isabelle นี่เอง

ทุกอย่างฟังดูดี
แต่ปัญหาของ compiler พันธุ์ดุ ก็คือ มันไม่เก่งเรื่องทำให้ code เร็วขึ้น

โปรเจคของเราคือ ดูซิว่ามีวิธีไหนบ้างที่เราจะช่วย compiler พันธุ์ดุ พวกนี้ทำให้ code เร็วขึ้นได้ยังไงบ้าง
แล้วก็ต้องอย่าลืม พิสูจน์ทางคณิตศาสตร์ด้วยว่า compiler ไม่มี bug

หนึ่งสัปดาห์ที่อยู่กับเจเรมี่ส่วนใหญ่ก็ฝึกการใช้ isabelle
กับการพิสูจน์พวกความถูกต้องของการ compile ง่ายๆ สำหรับภาษาโปรแกรมเล็กๆ

สรุป ซัมเมอร์นี้ ไม่เสียเปล่า
ได้เปิดหูเปิดตา กับอะไรที่เรารู้สึกว่า เจ๋งเป้ง
แล้วก็ได้ทำความคุ้นเคยกับการพิสูจน์แบบมีคอมพิวเตอร์ช่วย


กิจกรรม


เอาหละ หมดเรื่องน่าเบื่อ

เข้าเรื่องสนุกจริงๆ

ปิดเทอมใหญ่นี้เต็มไปด้วยการเดินทาง การออกกำลังกาย การลดน้ำหนัก และความทรงจำดีๆกับเพื่อน

เขียนอธิบายไม่หมด เลยเอารูปมาช่วย


ได้ไปงานรับปริญญาเพื่อน

10348892_714409118602853_166138335875418391_o


เตะบอลส่งท้ายก่อนเพื่อนบางคนกลับไทย

10382555_10152094612426931_6859195215141217389_o

10402663_10152195237541989_5485825932705488715_n


มีเพื่อนมานอนค้างที่บ้าน

10307185_10152158614781989_2038657115443100215_n

10580257_10152321871746989_1872341286910013179_n

ไม่ใช่แค่นั้น มีดู harry potter เรียงทุกภาค แต่ไม่ได้ถ่ายรูปบรรยากาศมา


ฟิตออกกำลังกาย

10306487_10152177963046989_5537982465445897122_n

10462826_10152472278287692_7606411862260377677_n

10487579_10152218248066989_6229168844624169676_n


ควบคุมอาหาร ลดน้ำหนัก

10464048_10152213709546989_6735124416626276595_n

10501763_10152288527906989_2113153872999099706_n

10356273_10152346707736989_4659651454085292205_n

ดั้งเดิมอยู่แถวๆ 73 กิโล


เคลียร์เกม final fantasy

10440847_10152204730386989_8834482802996157262_n


ได้ใบสั่งใบแรกในอเมริกา

10435835_10152269060316989_822649120493719186_n


ไปเยี่ยมเพื่อนซึ่งมีลูกหยกๆ (แต่ถ่ายรูปกับหมา)

10406424_10152258184101989_1462559298254228385_n


ไปเยี่ยมญาติ (แต่ถ่ายรูปกับแมว)

10574425_10152295149391989_6215851931809339062_n


พี่แอนมาเยี่ยม

10300010_10152170583501989_1925714937891262024_n


เยี่ยมเพื่อนเซนต์ดอมินิก

1555374_10152338742186989_7709696989319258635_n


สุดท้าย เยี่ยมเดียร์สองรอบเลย

10409242_10152235741641989_1829685893440094652_n

10590580_10152333525801989_835935099217987225_n


ตอนนี้เทอม 5 ละ จะพยายามอัพเดทเทอม 4 ก่อน เทอม 6 จะเริ่ม

ป.ล. ใครที่สงสัย โดยเฉลี่ยแล้วเรียนเอกจะมีประมาณ 15-21 เทอมนะ

Posted in: Uncategorized